# HG changeset patch
# User wenzelm
# Date 1692689324 -7200
# Node ID ca0fe2802123c757a6d0366b6dcc12cf067f4982
# Parent  131e2a220c78f14b6ac3abc62f66160a9007e061
tuned signature;

diff -r 131e2a220c78 -r ca0fe2802123 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Mon Aug 21 20:40:15 2023 +0200
+++ b/src/Pure/Tools/build.scala	Tue Aug 22 09:28:44 2023 +0200
@@ -505,9 +505,9 @@
   /* build_worker */
 
   def build_worker_command(
-    base_options: List[Options.Spec],
     host: Build_Cluster.Host,
     ssh: SSH.System = SSH.Local,
+    build_options: List[Options.Spec] = Nil,
     build_id: String = "",
     isabelle_home: Path = Path.current,
     afp_root: Option[Path] = None,
@@ -515,7 +515,7 @@
     verbose: Boolean = false
   ): String = {
     val options =
-      base_options ::: Options.Spec("build_hostname", Some(host.name)) :: host.options
+      build_options ::: Options.Spec("build_hostname", Some(host.name)) :: host.options
     ssh.bash_path(isabelle_home + Path.explode("bin/isabelle")) + " build_worker" +
       if_proper(build_id, " -B " + Bash.string(build_id)) +
       if_proper(afp_root, " -A " + ssh.bash_path(afp_root.get)) +
diff -r 131e2a220c78 -r ca0fe2802123 src/Pure/Tools/build_cluster.scala
--- a/src/Pure/Tools/build_cluster.scala	Mon Aug 21 20:40:15 2023 +0200
+++ b/src/Pure/Tools/build_cluster.scala	Tue Aug 22 09:28:44 2023 +0200
@@ -157,10 +157,9 @@
 
     def start(): Process_Result = {
       val script =
-        Build.build_worker_command(
-          List(options.check_name("build_database_server").spec),
-          host,
+        Build.build_worker_command(host,
           ssh = ssh,
+          build_options = List(options.check_name("build_database_server").spec),
           build_id = build_context.build_uuid,
           isabelle_home = remote_isabelle_home,
           afp_root = remote_afp_root)