src/Pure/ML-Systems/smlnj-0.93.ML
changeset 6227 3198f547f8af
parent 5816 6f3cb53502fa
child 7149 d0c2168f7704
--- a/src/Pure/ML-Systems/smlnj-0.93.ML	Thu Feb 04 18:15:01 1999 +0100
+++ b/src/Pure/ML-Systems/smlnj-0.93.ML	Thu Feb 04 18:15:20 1999 +0100
@@ -174,12 +174,11 @@
 
 (* file handling *)
 
-(*Get time of last modification; if file doesn't exist return an empty string*)
+(*get time of last modification*)
 local
   open System.Timer System.Unsafe.SysIO;
 in
-  fun file_info "" = ""
-    | file_info name = makestring (mtime (PATH name)) handle _ => "";
+  fun file_info name = makestring (mtime (PATH name)) handle _ => "";
 end;
 
 structure OS =