# HG changeset patch
# User wenzelm
# Date 1670755648 -3600
# Node ID e6c11ef4fb51962e46216ab20d7e46cf86dd66d0
# Parent  b865959e2547aa56a5b7f1e81dfbeefc304ee9b6
tuned signature;

diff -r b865959e2547 -r e6c11ef4fb51 src/Pure/General/mercurial.scala
--- a/src/Pure/General/mercurial.scala	Sat Dec 10 21:02:09 2022 +0100
+++ b/src/Pure/General/mercurial.scala	Sun Dec 11 11:47:28 2022 +0100
@@ -309,7 +309,7 @@
         Rsync.init(context0, target)
 
         val list =
-          Rsync.exec(context0, list = true, args = List("--", Rsync.terminate(target)))
+          Rsync.exec(context0, list = true, args = List("--", Rsync.direct(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.terminate(source), target)
+            Rsync.direct(source), target)
         ).check
       }
     }
diff -r b865959e2547 -r e6c11ef4fb51 src/Pure/General/rsync.scala
--- a/src/Pure/General/rsync.scala	Sat Dec 10 21:02:09 2022 +0100
+++ b/src/Pure/General/rsync.scala	Sun Dec 11 11:47:28 2022 +0100
@@ -59,12 +59,12 @@
             File.bash_path(init_dir) + "/.", target)).check
     }
 
-  def terminate(target: String): String =
-    if (target.endsWith(":") || target.endsWith("/")) target + "."
-    else if (target.endsWith(":.") || target.endsWith("/.")) target
-    else target + "/."
+  def direct(prefix: String): String =
+    if (prefix.endsWith(":") || prefix.endsWith("/")) prefix + "."
+    else if (prefix.endsWith(":.") || prefix.endsWith("/.")) prefix
+    else prefix + "/."
 
-  def append(target: String, rest: String): String =
-    if (target.endsWith(":") || target.endsWith("/")) target + rest
-    else target + "/" + rest
+  def append(prefix: String, suffix: String): String =
+    if (prefix.endsWith(":") || prefix.endsWith("/")) prefix + suffix
+    else prefix + "/" + suffix
 }