fixed file_info;
authorwenzelm
Thu, 04 Feb 1999 18:15:20 +0100
changeset 62273198f547f8af
parent 6226 42c94393d39e
child 6228 64f18b89d5d5
fixed file_info;
src/Pure/ML-Systems/mlworks.ML
src/Pure/ML-Systems/polyml.ML
src/Pure/ML-Systems/smlnj-0.93.ML
src/Pure/ML-Systems/smlnj.ML
     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 *)