# 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))) + }