src/Pure/Tools/build_job.scala
changeset 76871 a17f9ff37558
parent 76860 f95ed5a0600c
child 76872 8b98cffb1a99
--- 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("")