--- a/src/Pure/Tools/build.scala Sun Jul 23 21:04:33 2023 +0200
+++ b/src/Pure/Tools/build.scala Sun Jul 23 21:08:03 2023 +0200
@@ -513,13 +513,14 @@
dirs: List[Path] = Nil,
verbose: Boolean = false
): String = {
+ val 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)) +
dirs.map(dir => " -d " + ssh.bash_path(dir)).mkString +
if_proper(host.numa, " -N")
+ " -j" + host.jobs +
- host.options.map(opt => " -o " + Bash.string(Build_Cluster.Host.print_option(opt))).mkString +
+ options.map(opt => " -o " + Bash.string(Build_Cluster.Host.print_option(opt))).mkString +
if_proper(verbose, " -v")
}