# HG changeset patch
# User lcp
# Date 751219815 -3600
# Node ID 1b14cd9237726700730bd1d500e4d342aa56646c
# Parent  08d3c007ae7c368fb9daeab1e1822041fa01f46c
/NJ,POLY/delete_file: new

diff -r 08d3c007ae7c -r 1b14cd923772 src/Pure/NJ.ML
--- a/src/Pure/NJ.ML	Thu Oct 21 14:59:54 1993 +0100
+++ b/src/Pure/NJ.ML	Thu Oct 21 17:10:15 1993 +0100
@@ -79,7 +79,7 @@
   else f();
 
 
-(*** File information ***)
+(*** File handling ***)
 
 (*Get time of last modification.*)
 local
@@ -90,3 +90,5 @@
     | file_info name = makestring (mtime (PATH name));
 end;
 
+fun delete_file name = System.system ("rm " ^ name);
+
diff -r 08d3c007ae7c -r 1b14cd923772 src/Pure/POLY.ML
--- a/src/Pure/POLY.ML	Thu Oct 21 14:59:54 1993 +0100
+++ b/src/Pure/POLY.ML	Thu Oct 21 17:10:15 1993 +0100
@@ -36,7 +36,7 @@
     fn () => brk (99999, 0), en);
 
 
-(*** File information ***)
+(*** File handling ***)
 
 (*Get a string containing the time of last modification, attributes, owner
   and size of file (but not the path) *)
@@ -54,8 +54,10 @@
           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) *)
+             (*Remove the part after the last " " (i.e. the path/filename) *)
         in close_in is;
            close_out os;
            implode result
         end;
+
+fun delete_file name = ExtendedIO.execute ("rm " ^ name);