diff -r c6cdf2a641f4 -r a17f9ff37558 src/Pure/Tools/build_job.scala --- a/src/Pure/Tools/build_job.scala Mon Jan 02 15:41:50 2023 +0100 +++ b/src/Pure/Tools/build_job.scala Mon Jan 02 16:02:16 2023 +0100 @@ -246,6 +246,9 @@ val info: Sessions.Info = session_background.sessions_structure(session_name) val options: Options = NUMA.policy_options(info.options, numa_node) + val session_sources: Sessions.Sources.T = + Sessions.Sources.read_files(session_background.base, cache = store.cache.compress) + private val future_result: Future[Process_Result] = Future.thread("build", uninterruptible = true) { val parent = info.parent.getOrElse("")