simplified file_info by using System.filedate
authorclasohm
Tue Jan 09 13:45:58 1996 +0100 (1996-01-09)
changeset 1434834da5152421
parent 1433 e7f9273024c2
child 1435 aefcd255ed4a
simplified file_info by using System.filedate
src/Pure/POLY.ML
     1.1 --- a/src/Pure/POLY.ML	Sat Jan 06 14:04:12 1996 +0100
     1.2 +++ b/src/Pure/POLY.ML	Tue Jan 09 13:45:58 1996 +0100
     1.3 @@ -60,16 +60,7 @@
     1.4  (*Get a string containing the time of last modification, attributes, owner
     1.5    and size of file (but not the path) *)
     1.6  fun file_info "" = ""
     1.7 -  | file_info name =
     1.8 -      let
     1.9 -          val (is, os) = ExtendedIO.execute ("ls -l " ^ name)
    1.10 -          val (result, _) = take_suffix (apr(op<>," ")) 
    1.11 -                              (explode (ExtendedIO.input_line is))
    1.12 -             (*Remove the part after the last " " (i.e. the path/filename) *)
    1.13 -        in close_in is;
    1.14 -           close_out os;
    1.15 -           implode result
    1.16 -        end;
    1.17 +  | file_info name = string_of_int (System.filedate name);
    1.18  
    1.19  (*Delete a file *)
    1.20  fun delete_file name =