# HG changeset patch
# User wenzelm
# Date 1654973114 -7200
# Node ID be33ca6f45d7c47b25be87ed79ac1fbe1199448c
# Parent  4dd0f250ec0de204f4f03e0b7ba93bd640da38aa
more comments;

diff -r 4dd0f250ec0d -r be33ca6f45d7 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) +