# HG changeset patch # User wenzelm # Date 1654615440 -7200 # Node ID 96fb1f9a404285b0eef0b7ceb86f7a4af68c060c # Parent a66fd84a30b7003e564afc411813269fc46885c0 more robust: protect_args does not work with rsync 2.x from macOS, and is not required in typical situations; diff -r a66fd84a30b7 -r 96fb1f9a4042 src/Pure/Admin/build_history.scala --- a/src/Pure/Admin/build_history.scala Tue Jun 07 17:22:17 2022 +0200 +++ b/src/Pure/Admin/build_history.scala Tue Jun 07 17:24:00 2022 +0200 @@ -522,6 +522,7 @@ isabelle_other: Path, isabelle_identifier: String = "remote_build_history", progress: Progress = new Progress, + protect_args: Boolean = false, rev: String = "", afp_repos: Option[Path] = None, afp_rev: String = "", @@ -534,7 +535,7 @@ def sync_repos(target: Path, accurate: Boolean = false, rev: String = "", afp_rev: String = "", afp: Boolean = false ): Unit = { - val context = Rsync.Context(progress, port = ssh.port) + val context = Rsync.Context(progress, port = ssh.port, protect_args = protect_args) Sync_Repos.sync_repos(context, ssh.rsync_path(target), thorough = accurate, preserve_jars = !accurate, rev = rev, afp_rev = afp_rev, afp_root = if (afp) afp_repos else None)