# HG changeset patch # User wenzelm # Date 1536849007 -7200 # Node ID 6c1beb52d76669609b87870e26f8aa3f1732606e # Parent a319e3c522ba44d9c7842c8dc4219eabc5b18e02 more robust: avoid race condition wrt. cleanup of ML process, e.g. relevant for "$ISABELLE_TMP/rat.ML" in theory Codegen.Further; diff -r a319e3c522ba -r 6c1beb52d766 src/Pure/System/isabelle_system.scala --- a/src/Pure/System/isabelle_system.scala Thu Sep 13 16:15:05 2018 +0200 +++ b/src/Pure/System/isabelle_system.scala Thu Sep 13 16:30:07 2018 +0200 @@ -197,14 +197,16 @@ new SimpleFileVisitor[JPath] { override def visitFile(file: JPath, attrs: BasicFileAttributes): FileVisitResult = { - Files.deleteIfExists(file) + try { Files.deleteIfExists(file) } + catch { case _: IOException => } FileVisitResult.CONTINUE } override def postVisitDirectory(dir: JPath, e: IOException): FileVisitResult = { if (e == null) { - Files.deleteIfExists(dir) + try { Files.deleteIfExists(dir) } + catch { case _: IOException => } FileVisitResult.CONTINUE } else throw e