used unlink for delete_files instead of calling rm
authorclasohm
Mon, 10 Jan 1994 16:57:31 +0100
changeset 220 e50ea2471e06
parent 219 a2447b00517b
child 221 3886a320c5bc
used unlink for delete_files instead of calling rm
src/Pure/NJ.ML
--- a/src/Pure/NJ.ML	Mon Jan 10 13:22:54 1994 +0100
+++ b/src/Pure/NJ.ML	Mon Jan 10 16:57:31 1994 +0100
@@ -88,11 +88,9 @@
 in
   fun file_info "" = ""
     | file_info name = makestring (mtime (PATH name));
+
+  val delete_file = unlink;
 end;
 
-fun delete_file name = 
-  let val _ = System.system ("rm " ^ name)
-  in () end;
-
 (*Get pathname of current working directory *)
 fun pwd () = System.Directory.getWD ();