# HG changeset patch
# User wenzelm
# Date 1654622611 -7200
# Node ID fbe27a50706b551f42e8b5e11cdcf1b8f8ec7ca2
# Parent  7cdeed5dc96d52d9deedb9abb122444f0510e9a5
avoid noise via context.progress (amending 68162e4f60a7);

diff -r 7cdeed5dc96d -r fbe27a50706b src/Pure/General/mercurial.scala
--- a/src/Pure/General/mercurial.scala	Tue Jun 07 19:15:08 2022 +0200
+++ b/src/Pure/General/mercurial.scala	Tue Jun 07 19:23:31 2022 +0200
@@ -304,10 +304,12 @@
       require(ssh == SSH.Local, "local repository required")
 
       Isabelle_System.with_tmp_dir("sync") { tmp_dir =>
-        Rsync.init(context, target)
+        val context0 = context.copy(progress = new Progress)
+
+        Rsync.init(context0, target)
 
         val list =
-          Rsync.exec(context, list = true, args = List("--", Rsync.terminate(target)))
+          Rsync.exec(context0, list = true, args = List("--", Rsync.terminate(target)))
             .check.out_lines.filterNot(_.endsWith(" ."))
         if (list.nonEmpty && !list.exists(_.endsWith(Hg_Sync._NAME))) {
           error("No .hg_sync meta data in " + quote(target))
@@ -319,7 +321,7 @@
         val diff_content = if (is_changed) diff(rev = rev, options = "--git") else ""
         val stat_content = if (is_changed) diff(rev = rev, options = "--stat") else ""
 
-        Rsync.init(context, target,
+        Rsync.init(context0, target,
           contents =
             File.Content(Hg_Sync.PATH_ID, id_content) ::
             File.Content(Hg_Sync.PATH_LOG, log_content) ::