src/Pure/General/mercurial.scala
changeset 76617 d5adc9126ae8
parent 76616 e6c11ef4fb51
child 76883 186e07be32c3
--- a/src/Pure/General/mercurial.scala	Sun Dec 11 11:47:28 2022 +0100
+++ b/src/Pure/General/mercurial.scala	Sun Dec 11 12:52:46 2022 +0100
@@ -309,7 +309,7 @@
         Rsync.init(context0, target)
 
         val list =
-          Rsync.exec(context0, list = true, args = List("--", Rsync.direct(target)))
+          Rsync.exec(context0, list = true, args = List("--", Url.direct_path(target)))
             .check.out_lines.filterNot(_.endsWith(" ."))
         if (list.nonEmpty && !list.exists(_.endsWith(Hg_Sync._NAME))) {
           error("No .hg_sync meta data in " + quote(target))
@@ -355,7 +355,7 @@
           prune_empty_dirs = true,
           filter = protect ::: filter,
           args = List("--exclude-from=" + exclude_path.implode, "--",
-            Rsync.direct(source), target)
+            Url.direct_path(source), target)
         ).check
       }
     }