more robust: tmp files might get deleted concurrently in ML vs. Scala process;
--- 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