Standard_System.with_tmp_file: deleteOnExit to make double sure;
authorwenzelm
Wed, 22 Sep 2010 00:17:35 +0200
changeset 39582 a873158542d0
parent 39581 430ff865089b
child 39583 c1e9c6dfeff8
Standard_System.with_tmp_file: deleteOnExit to make double sure;
src/Pure/System/standard_system.scala
--- a/src/Pure/System/standard_system.scala	Tue Sep 21 22:16:22 2010 +0200
+++ b/src/Pure/System/standard_system.scala	Wed Sep 22 00:17:35 2010 +0200
@@ -101,6 +101,7 @@
   def with_tmp_file[A](prefix: String)(body: File => A): A =
   {
     val file = File.createTempFile(prefix, null)
+    file.deleteOnExit
     try { body(file) } finally { file.delete }
   }