diff -r c934f0e51f1c -r 36e6ba1527f0 src/Pure/System/isabelle_system.scala --- a/src/Pure/System/isabelle_system.scala Fri May 24 17:31:49 2024 +0200 +++ b/src/Pure/System/isabelle_system.scala Fri May 24 19:15:51 2024 +0200 @@ -181,10 +181,8 @@ else make_directory(path) def copy_dir(dir1: Path, dir2: Path, direct: Boolean = false): Unit = { - def make_path(dir: Path): String = { - val s = File.standard_path(dir.absolute) - if (direct) Url.direct_path(s) else s - } + def make_path(dir: Path): String = + Url.dir_path(File.standard_path(dir.absolute), direct = direct) val p1 = make_path(dir1) val p2 = make_path(dir2) make_directory(if (direct) dir2.absolute else dir2.absolute.dir)