--- 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 =