# 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)