--- 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)
}
--- 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 = {
--- 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)