src/Pure/General/rsync.scala
changeset 77517 ede77a627b3a
parent 77369 df17355f1e2c
child 77518 fda4da0f80f4
--- 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,