src/Pure/Admin/build_history.scala
changeset 77792 b81b2c50fc7c
parent 77787 b20ac2c26ea3
child 77799 3fb2c47a7605
--- a/src/Pure/Admin/build_history.scala	Sat Apr 08 19:02:51 2023 +0200
+++ b/src/Pure/Admin/build_history.scala	Sat Apr 08 19:32:09 2023 +0200
@@ -535,7 +535,6 @@
     clean_platform: Boolean = false,
     clean_archives: Boolean = false,
     progress: Progress = new Progress,
-    protect_args: Boolean = false,
     rev: String = "",
     afp_repos: Option[Path] = None,
     afp_rev: String = "",
@@ -548,7 +547,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, protect_args = protect_args)
+      val context = Rsync.Context(progress = progress, ssh = ssh)
       Sync.sync(ssh.options, context, target,
         thorough = accurate, preserve_jars = !accurate,
         rev = rev, afp_rev = afp_rev, afp_root = if (afp) afp_repos else None)