author | wenzelm |
Wed, 22 Sep 2010 00:17:35 +0200 | |
changeset 39582 | a873158542d0 |
parent 39581 | 430ff865089b |
child 39583 | c1e9c6dfeff8 |
--- 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 } }