src/Pure/General/rsync.scala
changeset 76131 8b695e59db3f
parent 75554 be33ca6f45d7
child 76136 1bb677cceea4
--- 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 "")
   }