int file_time(file)
string file

Return the date of the last write to the file in seconds since 1970.
This function is defined in /secure/simul_efun.c

See also time, ctime.
