# HG changeset patch
# User clasohm
# Date 821191558 -3600
# Node ID 834da5152421799142d30e5b8f9cd3a4b3319c77
# Parent  e7f9273024c2c4b052d3cef27ad8c167f3282bf2
simplified file_info by using System.filedate

diff -r e7f9273024c2 -r 834da5152421 src/Pure/POLY.ML
--- a/src/Pure/POLY.ML	Sat Jan 06 14:04:12 1996 +0100
+++ b/src/Pure/POLY.ML	Tue Jan 09 13:45:58 1996 +0100
@@ -60,16 +60,7 @@
 (*Get a string containing the time of last modification, attributes, owner
   and size of file (but not the path) *)
 fun file_info "" = ""
-  | file_info name =
-      let
-          val (is, os) = ExtendedIO.execute ("ls -l " ^ name)
-          val (result, _) = take_suffix (apr(op<>," ")) 
-                              (explode (ExtendedIO.input_line is))
-             (*Remove the part after the last " " (i.e. the path/filename) *)
-        in close_in is;
-           close_out os;
-           implode result
-        end;
+  | file_info name = string_of_int (System.filedate name);
 
 (*Delete a file *)
 fun delete_file name =