more robust (amending 87403fde8cc3): notably allow symlink to existing directory, which Files.createDirectories does not accept;
authorwenzelm
Sun, 28 Feb 2021 21:31:35 +0100
changeset 73572 a89f56ab2686
parent 73571 48abb09d49ea
child 73573 7a88313895d5
more robust (amending 87403fde8cc3): notably allow symlink to existing directory, which Files.createDirectories does not accept;
src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Sat Feb 27 22:17:56 2021 +0100
+++ b/src/Pure/System/isabelle_system.scala	Sun Feb 28 21:31:35 2021 +0100
@@ -208,8 +208,10 @@
 
   def make_directory(path: Path): Path =
   {
-    try { Files.createDirectories(path.file.toPath) }
-    catch { case ERROR(_) => error("Failed to create directory: " + path.absolute) }
+    if (!path.is_dir) {
+      try { Files.createDirectories(path.file.toPath) }
+      catch { case ERROR(_) => error("Failed to create directory: " + path.absolute) }
+    }
     path
   }