K 10 svn:author V 5 peter K 8 svn:date V 27 2003-10-26T04:45:08.000000Z K 7 svn:log V 145 Fix a 64 bit warning. Have set_T_dev_t() take a pointer to a size_t rather than a pointer to an int, since that is what it really wants anyway. END