int vm_serial= 25;
char *vm_version= "2.3";
char *vm_date= "Thu Mar 11 17:46:46 EST 1999";
char *cc_version= "cc";
char *ux_version= "IRIX stinkurd 6.3 12161207 IP32";