# HG changeset patch
# User wenzelm
# Date 1676109998 -3600
# Node ID f947e045fa61603ce9ef59476a17365d788fec5f
# Parent  dce91dab1728eec2253ffdc3898c32da1049219b
clarified signature;

diff -r dce91dab1728 -r f947e045fa61 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Wed Feb 08 10:18:30 2023 +0100
+++ b/src/Pure/Tools/build.scala	Sat Feb 11 11:06:38 2023 +0100
@@ -426,10 +426,15 @@
                   using(store.open_database(session_name, output = true))(
                     store.init_session_info(_, session_name))
 
+                  val session_background = build_deps.background(session_name)
+                  val resources =
+                    new Resources(session_background, log = log,
+                      command_timings = queue.command_timings(session_name))
+
                   val numa_node = numa_nodes.next(used_node)
                   val job =
-                    new Build_Job(progress, build_deps.background(session_name), store, do_store,
-                      log, session_setup, numa_node, queue.command_timings(session_name))
+                    new Build_Job(progress, session_background, store, do_store,
+                      resources, session_setup, numa_node)
                   loop(pending, running + (session_name -> (input_heaps, job)), results)
                 }
                 else {
diff -r dce91dab1728 -r f947e045fa61 src/Pure/Tools/build_job.scala
--- a/src/Pure/Tools/build_job.scala	Wed Feb 08 10:18:30 2023 +0100
+++ b/src/Pure/Tools/build_job.scala	Sat Feb 11 11:06:38 2023 +0100
@@ -239,10 +239,9 @@
   session_background: Sessions.Background,
   store: Sessions.Store,
   val do_store: Boolean,
-  log: Logger,
+  resources: Resources,
   session_setup: (String, Session) => Unit,
-  val numa_node: Option[Int],
-  command_timings0: List[Properties.T]
+  val numa_node: Option[Int]
 ) {
   def session_name: String = session_background.session_name
   val info: Sessions.Info = session_background.sessions_structure(session_name)
@@ -291,9 +290,6 @@
               }
         }
 
-      val resources =
-        new Resources(session_background, log = log, command_timings = command_timings0)
-
       val session =
         new Session(options, resources) {
           override val cache: Term.Cache = store.cache