tuned;
authorwenzelm
Tue, 07 Mar 2023 12:15:37 +0100
changeset 77558 2d06b514b363
parent 77557 eff08c3f89fe
child 77559 4ad322ee6025
tuned;
src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Tue Mar 07 12:06:01 2023 +0100
+++ b/src/Pure/Tools/build.scala	Tue Mar 07 12:15:37 2023 +0100
@@ -64,7 +64,10 @@
     engines.find(_.name == name).getOrElse(error("Bad build engine " + quote(name)))
 
 
-  /* build */
+  /* options */
+
+  def hostname(options: Options): String =
+    Isabelle_System.hostname(options.string("build_hostname"))
 
   def build_init(options: Options): Sessions.Store = {
     val build_options =
@@ -79,6 +82,9 @@
     store
   }
 
+
+  /* build */
+
   def build(
     options: Options,
     selection: Sessions.Selection = Sessions.Selection.empty,
@@ -158,9 +164,9 @@
 
     val build_context =
       Build_Process.Context(store, build_deps, progress = progress,
-        hostname = Isabelle_System.hostname(build_options.string("build_hostname")),
-        build_heap = build_heap, numa_shuffling = numa_shuffling, max_jobs = max_jobs,
-        fresh_build = fresh_build, no_build = no_build, session_setup = session_setup)
+        hostname = hostname(build_options), build_heap = build_heap,
+        numa_shuffling = numa_shuffling, max_jobs = max_jobs, fresh_build = fresh_build,
+        no_build = no_build, session_setup = session_setup)
 
     store.prepare_output()
     build_context.prepare_database()
@@ -322,10 +328,9 @@
 
       val start_date = Date.now()
 
-      val hostname = Isabelle_System.hostname(options.string("build_hostname"))
       progress.echo(
         "Started at " + Build_Log.print_date(start_date) +
-          " (" + Isabelle_System.getenv("ML_IDENTIFIER") + " on " + hostname +")",
+          " (" + Isabelle_System.getenv("ML_IDENTIFIER") + " on " + hostname(options) +")",
         verbose = true)
       progress.echo(Build_Log.Settings.show() + "\n", verbose = true)