--- a/src/Pure/General/rsync.scala Tue Sep 13 09:45:02 2022 +0200
+++ b/src/Pure/General/rsync.scala Tue Sep 13 09:59:08 2022 +0200
@@ -9,12 +9,12 @@
object Rsync {
sealed case class Context(progress: Progress,
- port: Int = SSH.default_port,
+ port: Int = 0,
archive: Boolean = true,
protect_args: Boolean = true // requires rsync 3.0.0, or later
) {
def command: String =
- "rsync --rsh=" + Bash.string("ssh -p " + port) +
+ "rsync --rsh=" + Bash.string("ssh" + (if (port > 0) "-p " + port else "")) +
(if (archive) " --archive" else "") +
(if (protect_args) " --protect-args" else "")
}