# HG changeset patch
# User clasohm
# Date 758217451 -3600
# Node ID e50ea2471e068d96d647f6ea894c7db49ce32530
# Parent  a2447b00517bc681cd123bb28060bc3219d68995
used unlink for delete_files instead of calling rm

diff -r a2447b00517b -r e50ea2471e06 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 ();