diff -r b703cecf9bd0 -r 8b695e59db3f src/Pure/General/rsync.scala --- 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 "") }