1.1 --- a/src/Pure/ML-Systems/mlworks.ML Thu Feb 04 18:15:01 1999 +0100
1.2 +++ b/src/Pure/ML-Systems/mlworks.ML Thu Feb 04 18:15:20 1999 +0100
1.3 @@ -124,9 +124,8 @@
1.4
1.5 (* file handling *)
1.6
1.7 -(*get time of last modification; if file doesn't exist return an empty string*)
1.8 -fun file_info "" = "" (* FIXME !? *)
1.9 - | file_info name = Time.toString (OS.FileSys.modTime name) handle _ => "";
1.10 +(*get time of last modification*)
1.11 +fun file_info name = Time.toString (OS.FileSys.modTime name) handle _ => "";
1.12
1.13
1.14 (* getenv *)
2.1 --- a/src/Pure/ML-Systems/polyml.ML Thu Feb 04 18:15:01 1999 +0100
2.2 +++ b/src/Pure/ML-Systems/polyml.ML Thu Feb 04 18:15:20 1999 +0100
2.3 @@ -109,9 +109,8 @@
2.4
2.5 (* file handling *)
2.6
2.7 -(*get time of last modification; if file doesn't exist return an empty string*)
2.8 -fun file_info "" = "" (* FIXME !? *)
2.9 - | file_info name = Int.toString (System.filedate name) handle _ => "";
2.10 +(*get time of last modification*)
2.11 +fun file_info name = Int.toString (System.filedate name) handle _ => "";
2.12
2.13 structure OS =
2.14 struct
3.1 --- a/src/Pure/ML-Systems/smlnj-0.93.ML Thu Feb 04 18:15:01 1999 +0100
3.2 +++ b/src/Pure/ML-Systems/smlnj-0.93.ML Thu Feb 04 18:15:20 1999 +0100
3.3 @@ -174,12 +174,11 @@
3.4
3.5 (* file handling *)
3.6
3.7 -(*Get time of last modification; if file doesn't exist return an empty string*)
3.8 +(*get time of last modification*)
3.9 local
3.10 open System.Timer System.Unsafe.SysIO;
3.11 in
3.12 - fun file_info "" = ""
3.13 - | file_info name = makestring (mtime (PATH name)) handle _ => "";
3.14 + fun file_info name = makestring (mtime (PATH name)) handle _ => "";
3.15 end;
3.16
3.17 structure OS =
4.1 --- a/src/Pure/ML-Systems/smlnj.ML Thu Feb 04 18:15:01 1999 +0100
4.2 +++ b/src/Pure/ML-Systems/smlnj.ML Thu Feb 04 18:15:20 1999 +0100
4.3 @@ -192,9 +192,8 @@
4.4
4.5 (* file handling *)
4.6
4.7 -(*get time of last modification; if file doesn't exist return an empty string*)
4.8 -fun file_info "" = "" (* FIXME !? *)
4.9 - | file_info name = Time.toString (OS.FileSys.modTime name) handle _ => "";
4.10 +(*get time of last modification*)
4.11 +fun file_info name = Time.toString (OS.FileSys.modTime name) handle _ => "";
4.12
4.13
4.14 (* getenv *)