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