proper symbolic hostname, as provided via Build_Cluster.Host;
authorwenzelm
Sun, 23 Jul 2023 21:08:03 +0200
changeset 78446 9067d8ac9c47
parent 78445 d70dc78c0d4e
child 78447 43cbd96de418
proper symbolic hostname, as provided via Build_Cluster.Host;
src/Pure/Tools/build.scala
--- 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")
   }