# 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 = {