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) }