removed file_info (now in Pure/General/file.ML);
authorwenzelm
Sun Jun 05 11:31:30 2005 +0200 (2005-06-05)
changeset 162667a6616be8712
parent 16265 ee2497cde564
child 16267 0773b17922d8
removed file_info (now in Pure/General/file.ML);
src/Pure/ML-Systems/mosml.ML
src/Pure/ML-Systems/polyml.ML
src/Pure/ML-Systems/smlnj.ML
     1.1 --- a/src/Pure/ML-Systems/mosml.ML	Sun Jun 05 11:31:29 2005 +0200
     1.2 +++ b/src/Pure/ML-Systems/mosml.ML	Sun Jun 05 11:31:30 2005 +0200
     1.3 @@ -124,12 +124,6 @@
     1.4    if Process.system cmd = Process.success then 0 else 1;
     1.5  
     1.6  
     1.7 -(* file handling *)
     1.8 -
     1.9 -(*get time of last modification*)
    1.10 -fun file_info name = Time.toString (FileSys.modTime name) handle _ => "";
    1.11 -
    1.12 -
    1.13  (* getenv *)
    1.14  
    1.15  fun getenv var =
     2.1 --- a/src/Pure/ML-Systems/polyml.ML	Sun Jun 05 11:31:29 2005 +0200
     2.2 +++ b/src/Pure/ML-Systems/polyml.ML	Sun Jun 05 11:31:30 2005 +0200
     2.3 @@ -151,12 +151,6 @@
     2.4    if OS.Process.isSuccess (OS.Process.system cmd) then 0 else 1;
     2.5  
     2.6  
     2.7 -(* file handling *)
     2.8 -
     2.9 -(*get time of last modification*)
    2.10 -fun file_info name = Time.toString (OS.FileSys.modTime name) handle _ => "";
    2.11 -
    2.12 -
    2.13  (* getenv *)
    2.14  
    2.15  fun getenv var =
     3.1 --- a/src/Pure/ML-Systems/smlnj.ML	Sun Jun 05 11:31:29 2005 +0200
     3.2 +++ b/src/Pure/ML-Systems/smlnj.ML	Sun Jun 05 11:31:30 2005 +0200
     3.3 @@ -180,12 +180,6 @@
     3.4  val system = OS.Process.system: string -> int;
     3.5  
     3.6  
     3.7 -(* file handling *)
     3.8 -
     3.9 -(*get time of last modification*)
    3.10 -fun file_info name = Time.toString (OS.FileSys.modTime name) handle _ => "";
    3.11 -
    3.12 -
    3.13  (* getenv *)
    3.14  
    3.15  fun getenv var =