| changeset 2304 | 618b545fe9c4 |
| parent 2288 | 16e7a5adb679 |
| child 2408 | acddf41dbbf7 |
--- a/src/Pure/NJ1xx.ML Tue Dec 03 11:20:43 1996 +0100 +++ b/src/Pure/NJ1xx.ML Tue Dec 03 11:21:47 1996 +0100 @@ -79,9 +79,7 @@ (*Get time of last modification; if file doesn't exist return an empty string*) fun file_info "" = "" - | file_info name = Time.toString - (Posix.FileSys.ST.mtime (Posix.FileSys.stat name)) - handle _ => ""; + | file_info name = Time.toString (OS.FileSys.modTime name) handle _ =>"";