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