# HG changeset patch
# User wenzelm
# Date 1670781461 -3600
# Node ID 247a51c3abec5e402eed092d5465d7bcd5616b60
# Parent  61dae67ad4dddbf037f0e3768237676dc64ea437
more uniform use of make_directory;

diff -r 61dae67ad4dd -r 247a51c3abec src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Sun Dec 11 18:50:21 2022 +0100
+++ b/src/Pure/System/isabelle_system.scala	Sun Dec 11 18:57:41 2022 +0100
@@ -169,7 +169,7 @@
     }
     val p1 = make_path(dir1)
     val p2 = make_path(dir2)
-    if (direct) make_directory(dir2)
+    make_directory(if (direct) dir2.absolute else dir2.absolute.dir)
     val res = bash("cp -a " + Bash.string(p1) + " " + Bash.string(p2))
     if (!res.ok) cat_error("Failed to copy " + quote(p1) + " to " + quote(p2), res.err)
   }