--- 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);
+
--- 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);