src/Pure/General/mercurial.scala
changeset 75509 b22228173915
parent 75507 a5e0f1c66c26
child 75510 0106c89fb71f
--- a/src/Pure/General/mercurial.scala	Wed Jun 01 10:07:00 2022 +0200
+++ b/src/Pure/General/mercurial.scala	Wed Jun 01 10:10:42 2022 +0200
@@ -540,8 +540,8 @@
             case Some(dir) => repository(dir)
             case None => the_repository(Path.current)
           }
-        hg.sync(target, progress = progress, port = port, verbose = verbose, thorough = thorough,
-          dry_run = dry_run, clean = clean, filter = filter, rev = rev)
+        hg.sync(target, progress = progress, port = port, verbose = verbose || dry_run,
+          thorough = thorough, dry_run = dry_run, clean = clean, filter = filter, rev = rev)
       }
     )
 }