# HG changeset patch # User wenzelm # Date 1670763912 -3600 # Node ID fb322b989584401e2e73e53785b897f3e88b14b6 # Parent 87d0aab3a8e47f431137b744e20ff0a5b51e6b20 more robust; diff -r 87d0aab3a8e4 -r fb322b989584 src/Pure/System/isabelle_system.scala --- a/src/Pure/System/isabelle_system.scala Sun Dec 11 13:54:16 2022 +0100 +++ b/src/Pure/System/isabelle_system.scala Sun Dec 11 14:05:12 2022 +0100 @@ -163,10 +163,13 @@ else make_directory(path) def copy_dir(dir1: Path, dir2: Path): Unit = { - val res = bash("cp -a " + File.bash_path(dir1) + " " + File.bash_path(dir2)) - if (!res.ok) { - cat_error("Failed to copy directory " + dir1.absolute + " to " + dir2.absolute, res.err) + def make_path(dir: Path): String = { + File.standard_path(dir.absolute) } + val p1 = make_path(dir1) + val p2 = make_path(dir2) + 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) } def with_copy_dir[A](dir1: Path, dir2: Path)(body: => A): A = {