# HG changeset patch
# User wenzelm
# Date 1676978015 -3600
# Node ID 0bec014c0f9fe187ad2bc99d8ce15b55c4d81779
# Parent  1a5ee9b70de9a33516eafb3f1a10c160a43c978a
tuned signature;

diff -r 1a5ee9b70de9 -r 0bec014c0f9f src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Tue Feb 21 12:11:13 2023 +0100
+++ b/src/Pure/Tools/build_process.scala	Tue Feb 21 12:13:35 2023 +0100
@@ -193,11 +193,13 @@
 
   // global state
   protected var _numa_index = 0
-  protected var _pending: List[Build_Process.Entry] =
+  protected var _pending: List[Build_Process.Entry] = init_pending()
+  protected var _running = Map.empty[String, Build_Job]
+  protected var _results = Map.empty[String, Build_Process.Result]
+
+  protected def init_pending(): List[Build_Process.Entry] =
     (for ((name, (_, (preds, _))) <- build_context.sessions_structure.build_graph.iterator)
       yield Build_Process.Entry(name, preds.toList)).toList
-  protected var _running = Map.empty[String, Build_Job]
-  protected var _results = Map.empty[String, Build_Process.Result]
 
   protected def is_pending(): Boolean = synchronized { _pending.nonEmpty }