--- 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 {
--- 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