src/Pure/Admin/build_history.scala
changeset 76136 1bb677cceea4
parent 76122 b8f26c20d3b1
child 76351 2cee31cd92f0
--- a/src/Pure/Admin/build_history.scala	Tue Sep 13 10:44:47 2022 +0200
+++ b/src/Pure/Admin/build_history.scala	Tue Sep 13 11:56:38 2022 +0200
@@ -535,7 +535,9 @@
     def sync(target: Path, accurate: Boolean = false,
       rev: String = "", afp_rev: String = "", afp: Boolean = false
     ): Unit = {
-      val context = Rsync.Context(progress, port = ssh.port, protect_args = protect_args)
+      val context =
+        Rsync.Context(progress, ssh_port = ssh.port, ssh_control_path = ssh.control_path,
+          protect_args = protect_args)
       Sync.sync(ssh.options, context, ssh.rsync_path(target),
         thorough = accurate, preserve_jars = !accurate,
         rev = rev, afp_rev = afp_rev, afp_root = if (afp) afp_repos else None)