# HG changeset patch
# User wenzelm
# Date 1654613277 -7200
# Node ID ff8012edac89d445800d2d6c60170c3ae4747fe9
# Parent  0dcaf0e5107b81dc5d276d608b59d19fe877a88b
clarified signature;

diff -r 0dcaf0e5107b -r ff8012edac89 src/Pure/Admin/sync_repos.scala
--- a/src/Pure/Admin/sync_repos.scala	Tue Jun 07 12:32:53 2022 +0200
+++ b/src/Pure/Admin/sync_repos.scala	Tue Jun 07 16:47:57 2022 +0200
@@ -38,7 +38,7 @@
 
     for (hg <- afp_hg) {
       progress.echo_if(verbose, "\n* AFP repository:")
-      sync(hg, Rsync.rsync_dir(target) + "/AFP", afp_rev)
+      sync(hg, Rsync.append(target, "AFP"), afp_rev)
     }
   }
 
diff -r 0dcaf0e5107b -r ff8012edac89 src/Pure/General/mercurial.scala
--- a/src/Pure/General/mercurial.scala	Tue Jun 07 12:32:53 2022 +0200
+++ b/src/Pure/General/mercurial.scala	Tue Jun 07 16:47:57 2022 +0200
@@ -310,7 +310,7 @@
 
         val list =
           Rsync.rsync(port = port, list = true,
-            args = List("--", Rsync.rsync_dir(target))
+            args = List("--", Rsync.terminate(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.rsync_dir(source), target)
+            Rsync.terminate(source), target)
         ).check
       }
     }
diff -r 0dcaf0e5107b -r ff8012edac89 src/Pure/General/rsync.scala
--- a/src/Pure/General/rsync.scala	Tue Jun 07 12:32:53 2022 +0200
+++ b/src/Pure/General/rsync.scala	Tue Jun 07 16:47:57 2022 +0200
@@ -33,12 +33,6 @@
     progress.bash(script, echo = true)
   }
 
-  def rsync_dir(target: String): String = {
-    if (target.endsWith(":.") || target.endsWith("/.")) target
-    else if (target.endsWith(":") || target.endsWith("/")) target + "."
-    else target + "/."
-  }
-
   def rsync_init(target: String,
     port: Int = SSH.default_port,
     contents: List[File.Content] = Nil
@@ -49,4 +43,13 @@
       rsync(port = port, thorough = true,
         args = List(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 append(target: String, rest: String): String =
+    if (target.endsWith(":") || target.endsWith("/")) target + rest
+    else target + "/" + rest
 }