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