--- a/src/Pure/Tools/build_job.scala Mon Jan 02 20:24:43 2023 +0100
+++ b/src/Pure/Tools/build_job.scala Mon Jan 02 20:39:21 2023 +0100
@@ -246,8 +246,8 @@
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)
+ val session_sources: Sessions.Sources =
+ Sessions.Sources.load(session_background.base, cache = store.cache.compress)
private val future_result: Future[Process_Result] =
Future.thread("build", uninterruptible = true) {