# HG changeset patch
# User wenzelm
# Date 1430835926 -7200
# Node ID 2a5dbad7535522c35942708ccc1b9a98347917a8
# Parent  1470c081b49c62983680aec5154fe95c7ed1440e
more portable mkdirs via perl, e.g. relevant for Windows UNC paths (network shares);

diff -r 1470c081b49c -r 2a5dbad75355 src/Pure/System/isabelle_system.ML
--- a/src/Pure/System/isabelle_system.ML	Mon May 04 22:12:54 2015 +0200
+++ b/src/Pure/System/isabelle_system.ML	Tue May 05 16:25:26 2015 +0200
@@ -59,8 +59,10 @@
 (* directory operations *)
 
 fun mkdirs path =
-  if File.is_dir path orelse #rc (Bash.process ("mkdir -p " ^ File.shell_path path)) = 0 then ()
-  else error ("Failed to create directory: " ^ Path.print path);
+  if File.is_dir path then ()
+  else
+   (bash ("perl -e \"use File::Path make_path; make_path(" ^ File.shell_path path ^ ");\"");
+    if File.is_dir path then () else error ("Failed to create directory: " ^ Path.print path));
 
 fun mkdir path =
   if File.is_dir path then () else OS.FileSys.mkDir (File.platform_path path);
diff -r 1470c081b49c -r 2a5dbad75355 src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Mon May 04 22:12:54 2015 +0200
+++ b/src/Pure/System/isabelle_system.scala	Tue May 05 16:25:26 2015 +0200
@@ -258,8 +258,10 @@
   /* mkdirs */
 
   def mkdirs(path: Path): Unit =
-    if (path.is_dir || bash("mkdir -p " + shell_path(path)).rc == 0) ()
-    else error("Failed to create directory: " + quote(platform_path(path)))
+    if (!path.is_dir) {
+      bash("perl -e \"use File::Path make_path; make_path(" + shell_path(path) + ");\"")
+      if (!path.is_dir) error("Failed to create directory: " + quote(platform_path(path)))
+    }