more robust: tmp files might get deleted concurrently in ML vs. Scala process;
authorwenzelm
Thu, 02 Mar 2017 17:08:18 +0100
changeset 65090 fc8bb68a7439
parent 65089 1d219d76873b
child 65091 f7aaf4ce55a9
more robust: tmp files might get deleted concurrently in ML vs. Scala process;
src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Thu Mar 02 16:46:22 2017 +0100
+++ b/src/Pure/System/isabelle_system.scala	Thu Mar 02 17:08:18 2017 +0100
@@ -209,14 +209,14 @@
         new SimpleFileVisitor[JPath] {
           override def visitFile(file: JPath, attrs: BasicFileAttributes): FileVisitResult =
           {
-            Files.delete(file)
+            Files.deleteIfExists(file)
             FileVisitResult.CONTINUE
           }
 
           override def postVisitDirectory(dir: JPath, e: IOException): FileVisitResult =
           {
             if (e == null) {
-              Files.delete(dir)
+              Files.deleteIfExists(dir)
               FileVisitResult.CONTINUE
             }
             else throw e