# HG changeset patch
# User wenzelm
# Date 1614544295 -3600
# Node ID a89f56ab26863844d640938259ebee12905eca2b
# Parent  48abb09d49ea728f07e418bcb5e656d595c6169c
more robust (amending 87403fde8cc3): notably allow symlink to existing directory, which Files.createDirectories does not accept;

diff -r 48abb09d49ea -r a89f56ab2686 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
   }