# HG changeset patch
# User wenzelm
# Date 1680978090 -7200
# Node ID 4c4bd44ff683e5cf7dad69852722f4af07b7f0ac
# Parent  89e4971df8109466dcd32e72722e2c1c21ac9d85
more options;

diff -r 89e4971df810 -r 4c4bd44ff683 src/Pure/General/mercurial.scala
--- a/src/Pure/General/mercurial.scala	Sat Apr 08 19:36:03 2023 +0200
+++ b/src/Pure/General/mercurial.scala	Sat Apr 08 20:21:30 2023 +0200
@@ -608,7 +608,7 @@
           }
 
         using(SSH.open_system(options, host = ssh_host, port = ssh_port, user = ssh_user)) { ssh =>
-          val context = Rsync.Context(progress = progress, ssh = ssh)
+          val context = Rsync.Context(progress = progress, ssh = ssh, stats = verbose)
           hg.sync(context, target, thorough = thorough, dry_run = dry_run,
             filter = filter, rev = rev)
         }
diff -r 89e4971df810 -r 4c4bd44ff683 src/Pure/General/rsync.scala
--- a/src/Pure/General/rsync.scala	Sat Apr 08 19:36:03 2023 +0200
+++ b/src/Pure/General/rsync.scala	Sat Apr 08 20:21:30 2023 +0200
@@ -12,10 +12,11 @@
     def apply(
       progress: Progress = new Progress,
       ssh: SSH.System = SSH.Local,
-      archive: Boolean = true
+      archive: Boolean = true,
+      stats: Boolean = true
     ): Context = {
       val directory = Components.provide(Component_Rsync.home, ssh = ssh, progress = progress)
-      new Context(directory, progress, archive)
+      new Context(directory, progress, archive, stats)
     }
   }
 
@@ -23,11 +24,12 @@
     directory: Components.Directory,
     val progress: Progress,
     archive: Boolean,
+    stats: Boolean
   ) {
     override def toString: String = directory.toString
 
-    def no_progress: Context = new Context(directory, new Progress, archive)
-    def no_archive: Context = new Context(directory, progress, false)
+    def no_progress: Context = new Context(directory, new Progress, archive, stats)
+    def no_archive: Context = new Context(directory, progress, false, stats)
 
     def ssh: SSH.System = directory.ssh
 
@@ -37,7 +39,8 @@
       File.bash_path(Component_Rsync.local_program) + " --secluded-args" +
         if_proper(ssh_command, " --rsh=" + Bash.string(ssh_command)) +
         " --rsync-path=" + Bash.string(quote(File.standard_path(program))) +
-        (if (archive) " --archive" else "")
+        (if (archive) " --archive" else "") +
+        (if (stats) " --stats" else "")
     }
 
     def target(path: Path, direct: Boolean = false): String = {
diff -r 89e4971df810 -r 4c4bd44ff683 src/Pure/Tools/sync.scala
--- a/src/Pure/Tools/sync.scala	Sat Apr 08 19:36:03 2023 +0200
+++ b/src/Pure/Tools/sync.scala	Sat Apr 08 20:21:30 2023 +0200
@@ -139,7 +139,7 @@
         val progress = new Console_Progress(verbose = verbose)
 
         using(SSH.open_system(options, host = ssh_host, port = ssh_port, user = ssh_user)) { ssh =>
-          val context = Rsync.Context(progress = progress, ssh = ssh)
+          val context = Rsync.Context(progress = progress, ssh = ssh, stats = verbose)
           sync(options, context, target, thorough = thorough, purge_heaps = purge_heaps,
             session_images = session_images, preserve_jars = preserve_jars, dry_run = dry_run,
             rev = rev, afp_root = afp_root, afp_rev = afp_rev)