--- 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)) +
--- 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)