src/Pure/General/rsync.scala
changeset 77369 df17355f1e2c
parent 76617 d5adc9126ae8
child 77517 ede77a627b3a
--- a/src/Pure/General/rsync.scala	Fri Feb 24 20:40:50 2023 +0100
+++ b/src/Pure/General/rsync.scala	Fri Feb 24 20:52:35 2023 +0100
@@ -42,7 +42,7 @@
         (if (clean) " --delete-excluded" else "") +
         (if (list) " --list-only --no-human-readable" else "") +
         filter.map(s => " --filter=" + Bash.string(s)).mkString +
-        (if (args.nonEmpty) " " + Bash.strings(args) else "")
+        if_proper(args, " " + Bash.strings(args))
     context.progress.bash(script, echo = true)
   }