more portable mkdirs via perl, e.g. relevant for Windows UNC paths (network shares);
authorwenzelm
Tue, 05 May 2015 16:25:26 +0200
changeset 60263 2a5dbad75355
parent 60262 1470c081b49c
child 60264 96f8092fdd77
more portable mkdirs via perl, e.g. relevant for Windows UNC paths (network shares);
src/Pure/System/isabelle_system.ML
src/Pure/System/isabelle_system.scala
--- 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);
--- 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)))
+    }