# HG changeset patch # User wenzelm # Date 1692626048 -7200 # Node ID 20360824863a21d527c4e00d6abb40c755b46164 # Parent 754bfc558d212e05d249763c0fdecd72b547737a more robust command options; diff -r 754bfc558d21 -r 20360824863a src/Pure/System/options.scala --- 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 { diff -r 754bfc558d21 -r 20360824863a src/Pure/Tools/build.scala --- 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)) + diff -r 754bfc558d21 -r 20360824863a src/Pure/Tools/build_cluster.scala --- 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)