# HG changeset patch
# User wenzelm
# Date 1654615337 -7200
# Node ID a66fd84a30b7003e564afc411813269fc46885c0
# Parent  57b6a28e4ebada9174b20a8ddc145aa1c89f7e26
clarified context with global defaults;

diff -r 57b6a28e4eba -r a66fd84a30b7 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(