--- 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)
}
}
--- 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
}
}
--- 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
}