more robust: protect_args does not work with rsync 2.x from macOS, and is not required in typical situations;
authorwenzelm
Tue, 07 Jun 2022 17:24:00 +0200
changeset 75528 96fb1f9a4042
parent 75527 a66fd84a30b7
child 75529 31abccc97ade
more robust: protect_args does not work with rsync 2.x from macOS, and is not required in typical situations;
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)