# HG changeset patch
# User wenzelm
# Date 1676281773 -3600
# Node ID d060545f01a29e8ed95dc07b8120e4f213cb7fab
# Parent  6435b0fd48b55efe892e1d4902c3b4ea51fe5971
tuned;

diff -r 6435b0fd48b5 -r d060545f01a2 src/Pure/Tools/build_process.scala
--- 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