int vm_serial= 8;
char *vm_version= "2.3";
char *vm_date= "Fri Feb  5 18:53:14 EST 1999";
char *cc_version= "cc";
char *ux_version= "IRIX stinkurd 6.3 12161207 IP32";