src/Pure/General/rsync.scala
changeset 75554 be33ca6f45d7
parent 75534 1d937b12204d
child 76131 8b695e59db3f
--- a/src/Pure/General/rsync.scala	Fri Jun 10 23:53:09 2022 +0200
+++ b/src/Pure/General/rsync.scala	Sat Jun 11 20:45:14 2022 +0200
@@ -11,7 +11,7 @@
   sealed case class Context(progress: Progress,
     port: Int = SSH.default_port,
     archive: Boolean = true,
-    protect_args: Boolean = true
+    protect_args: Boolean = true  // requires rsync 3.0.0, or later
   ) {
     def command: String =
       "rsync --rsh=" + Bash.string("ssh -p " + port) +