# HG changeset patch
# User wenzelm
# Date 1716574994 -7200
# Node ID ed8a3f4e3de732924dfbdbc9bce6d658d10191e7
# Parent  36e6ba1527f0d0d47a34fad0ddbac0c9c882102b
tuned;

diff -r 36e6ba1527f0 -r ed8a3f4e3de7 src/Pure/Admin/build_history.scala
--- a/src/Pure/Admin/build_history.scala	Fri May 24 19:15:51 2024 +0200
+++ b/src/Pure/Admin/build_history.scala	Fri May 24 20:23:14 2024 +0200
@@ -546,8 +546,7 @@
     def sync(target: Path, accurate: Boolean = false,
       rev: String = "", afp_rev: String = "", afp: Boolean = false
     ): Unit = {
-      val context = Rsync.Context(progress = progress, ssh = ssh)
-      Sync.sync(ssh.options, context, target,
+      Sync.sync(ssh.options, Rsync.Context(progress = progress, ssh = ssh), target,
         thorough = accurate, preserve_jars = !accurate,
         rev = rev, afp_rev = afp_rev, afp_root = if (afp) afp_repos else None)
     }