--- a/src/Pure/Tools/build_process.scala Mon Feb 13 10:49:27 2023 +0100
+++ b/src/Pure/Tools/build_process.scala Mon Feb 13 10:49:33 2023 +0100
@@ -160,6 +160,13 @@
private val build_deps = build_context.deps
private val progress = build_context.progress
+ private val log =
+ build_options.string("system_log") match {
+ case "" => No_Logger
+ case "-" => Logger.make(progress)
+ case log_file => Logger.make(Some(Path.explode(log_file)))
+ }
+
// global state
private val numa_nodes = new NUMA.Nodes(numa_shuffling)
private var build_graph = build_context.sessions_structure.build_graph
@@ -167,13 +174,6 @@
private var running = Map.empty[String, Build_Job]
private var results = Map.empty[String, Build_Process.Result]
- private val log =
- build_options.string("system_log") match {
- case "" => No_Logger
- case "-" => Logger.make(progress)
- case log_file => Logger.make(Some(Path.explode(log_file)))
- }
-
private def remove_pending(name: String): Unit = {
build_graph = build_graph.del_node(name)
build_order = build_order - name