--- a/src/Pure/Admin/build_history.scala Fri Jun 10 15:34:25 2022 +0200
+++ b/src/Pure/Admin/build_history.scala Fri Jun 10 21:05:31 2022 +0200
@@ -536,7 +536,7 @@
rev: String = "", afp_rev: String = "", afp: Boolean = false
): Unit = {
val context = Rsync.Context(progress, port = ssh.nominal_port, protect_args = protect_args)
- Sync.sync(context, ssh.rsync_path(target),
+ 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)
}