diff -r e6c11ef4fb51 -r d5adc9126ae8 src/Pure/General/rsync.scala --- a/src/Pure/General/rsync.scala Sun Dec 11 11:47:28 2022 +0100 +++ b/src/Pure/General/rsync.scala Sun Dec 11 12:52:46 2022 +0100 @@ -58,13 +58,4 @@ List(if (contents.nonEmpty) "--archive" else "--dirs", File.bash_path(init_dir) + "/.", target)).check } - - def direct(prefix: String): String = - if (prefix.endsWith(":") || prefix.endsWith("/")) prefix + "." - else if (prefix.endsWith(":.") || prefix.endsWith("/.")) prefix - else prefix + "/." - - def append(prefix: String, suffix: String): String = - if (prefix.endsWith(":") || prefix.endsWith("/")) prefix + suffix - else prefix + "/" + suffix }