diff -r 71e3e144dc08 -r ede77a627b3a src/Pure/General/rsync.scala --- a/src/Pure/General/rsync.scala Sun Mar 05 15:19:53 2023 +0100 +++ b/src/Pure/General/rsync.scala Sun Mar 05 15:25:02 2023 +0100 @@ -33,6 +33,7 @@ filter: List[String] = Nil, args: List[String] = Nil ): Process_Result = { + val progress = context.progress val script = context.command + (if (verbose) " --verbose" else "") + @@ -43,7 +44,7 @@ (if (list) " --list-only --no-human-readable" else "") + filter.map(s => " --filter=" + Bash.string(s)).mkString + if_proper(args, " " + Bash.strings(args)) - context.progress.bash(script, echo = true) + progress.bash(script, echo = true) } def init(context: Context, target: String,