src/Pure/General/rsync.scala
changeset 76616 e6c11ef4fb51
parent 76170 5912209b4fb6
child 76617 d5adc9126ae8
--- 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
 }