# HG changeset patch # User wenzelm # Date 1678187737 -3600 # Node ID 2d06b514b3633b2ea22c9e305152c2c45218e192 # Parent eff08c3f89fe143c45eaba9548fadd4bb28b4300 tuned; diff -r eff08c3f89fe -r 2d06b514b363 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)