--- a/src/Pure/System/options.scala Mon Aug 21 15:28:35 2023 +0200
+++ b/src/Pure/System/options.scala Mon Aug 21 15:54:08 2023 +0200
@@ -83,6 +83,8 @@
description: String,
section: String
) {
+ def spec: Spec = Spec(name, Some(value))
+
private def print_value(x: String): String = if (typ == Options.String) quote(x) else x
private def print_standard: String =
standard_value match {
--- a/src/Pure/Tools/build.scala Mon Aug 21 15:28:35 2023 +0200
+++ b/src/Pure/Tools/build.scala Mon Aug 21 15:54:08 2023 +0200
@@ -505,6 +505,7 @@
/* build_worker */
def build_worker_command(
+ base_options: List[Options.Spec],
host: Build_Cluster.Host,
ssh: SSH.System = SSH.Local,
build_id: String = "",
@@ -513,7 +514,8 @@
dirs: List[Path] = Nil,
verbose: Boolean = false
): String = {
- val options = Options.Spec("build_hostname", Some(host.name)) :: host.options
+ val options =
+ base_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 15:28:35 2023 +0200
+++ b/src/Pure/Tools/build_cluster.scala Mon Aug 21 15:54:08 2023 +0200
@@ -157,7 +157,10 @@
def start(): Process_Result = {
val script =
- Build.build_worker_command(host, ssh = ssh,
+ Build.build_worker_command(
+ List(options.check_name("build_database_server").spec),
+ host,
+ ssh = ssh,
build_id = build_context.build_uuid,
isabelle_home = remote_isabelle_home,
afp_root = remote_afp_root)