more comments;
authorwenzelm
Sat, 11 Jun 2022 20:45:14 +0200
changeset 75554 be33ca6f45d7
parent 75553 4dd0f250ec0d
child 75555 197a5b3a1ea2
more comments;
src/Pure/General/rsync.scala
--- 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) +