# HG changeset patch
# User wenzelm
# Date 1654071042 -7200
# Node ID b22228173915ca94ea56d0a875d90afdd7e4a766
# Parent  64d48fb1b37b42558aba2bedb9d036b1da6bc2e1
clarified options;

diff -r 64d48fb1b37b -r b22228173915 src/Pure/Admin/sync_repos.scala
--- a/src/Pure/Admin/sync_repos.scala	Wed Jun 01 10:07:00 2022 +0200
+++ b/src/Pure/Admin/sync_repos.scala	Wed Jun 01 10:10:42 2022 +0200
@@ -28,7 +28,7 @@
     val more_filter = if (preserve_jars) List("include *.jar", "protect *.jar") else Nil
 
     def sync(hg: Mercurial.Repository, dest: String, r: String, filter: List[String] = Nil): Unit =
-      hg.sync(dest, rev = r, progress = progress, port = port, verbose = verbose,
+      hg.sync(dest, rev = r, progress = progress, port = port, verbose = verbose || dry_run,
         thorough = thorough, dry_run = dry_run, clean = clean, filter = filter ::: more_filter)
 
     progress.echo("\n* Isabelle repository:")
diff -r 64d48fb1b37b -r b22228173915 src/Pure/General/mercurial.scala
--- 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)
       }
     )
 }
diff -r 64d48fb1b37b -r b22228173915 src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Wed Jun 01 10:07:00 2022 +0200
+++ b/src/Pure/System/isabelle_system.scala	Wed Jun 01 10:10:42 2022 +0200
@@ -433,7 +433,7 @@
   ): Process_Result = {
     val script =
       "rsync --protect-args --archive --rsh=" + Bash.string("ssh -p " + port) +
-        (if (verbose || dry_run) " --verbose" else "") +
+        (if (verbose) " --verbose" else "") +
         (if (thorough) " --ignore-times" else " --omit-dir-times") +
         (if (dry_run) " --dry-run" else "") +
         (if (clean) " --delete-excluded" else "") +