src/Pure/NJ.ML
Mon, 10 Jan 1994 16:57:31 +0100 clasohm used unlink for delete_files instead of calling rm
Tue, 09 Nov 1993 14:24:45 +0100 clasohm fixed a bug in POLY.ML: delete_file didn't close streams;
Fri, 22 Oct 1993 13:39:23 +0100 clasohm delete_file now has type string -> unit in both NJ and POLY,
Thu, 21 Oct 1993 17:10:15 +0100 lcp /NJ,POLY/delete_file: new
Mon, 04 Oct 1993 15:36:31 +0100 wenzelm Pure/ROOT.ML
Thu, 16 Sep 1993 12:20:38 +0200 clasohm Initial revision
less more (0) tip