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