clarified context with global defaults;
authorwenzelm
Tue, 07 Jun 2022 17:22:17 +0200
changeset 75527 a66fd84a30b7
parent 75526 57b6a28e4eba
child 75528 96fb1f9a4042
clarified context with global defaults;
src/Pure/General/rsync.scala
--- a/src/Pure/General/rsync.scala	Tue Jun 07 17:10:51 2022 +0200
+++ b/src/Pure/General/rsync.scala	Tue Jun 07 17:22:17 2022 +0200
@@ -8,9 +8,15 @@
 
 
 object Rsync {
-  sealed case class Context(progress: Progress, port: Int = SSH.default_port) {
+  sealed case class Context(progress: Progress,
+    port: Int = SSH.default_port,
+    archive: Boolean = true,
+    protect_args: Boolean = true
+  ) {
     def command: String =
-      "rsync --protect-args --archive --rsh=" + Bash.string("ssh -p " + port)
+      "rsync --rsh=" + Bash.string("ssh -p " + port) +
+        (if (archive) " --archive" else "") +
+        (if (protect_args) " --protect-args" else "")
   }
 
   def exec(