changeset 6227 | 3198f547f8af |
parent 5816 | 6f3cb53502fa |
child 7855 | 092a6435afad |
--- a/src/Pure/ML-Systems/smlnj.ML Thu Feb 04 18:15:01 1999 +0100 +++ b/src/Pure/ML-Systems/smlnj.ML Thu Feb 04 18:15:20 1999 +0100 @@ -192,9 +192,8 @@ (* file handling *) -(*get time of last modification; if file doesn't exist return an empty string*) -fun file_info "" = "" (* FIXME !? *) - | file_info name = Time.toString (OS.FileSys.modTime name) handle _ => ""; +(*get time of last modification*) +fun file_info name = Time.toString (OS.FileSys.modTime name) handle _ => ""; (* getenv *)