--- a/src/Pure/Build/build_job.scala Tue Jun 24 21:32:51 2025 +0200
+++ b/src/Pure/Build/build_job.scala Tue Jun 24 21:49:43 2025 +0200
@@ -172,13 +172,12 @@
val session =
new Session(options) {
+ override val store: Store = store
+
override val resources: Resources =
new Resources(session_background, log = log,
command_timings =
- Properties.uncompress(
- session_context.old_command_timings_blob, cache = store.cache))
-
- override val cache: Rich_Text.Cache = store.cache
+ Properties.uncompress(session_context.old_command_timings_blob, cache = cache))
override def build_blobs_info(node_name: Document.Node.Name): Command.Blobs_Info =
Command.Blobs_Info.make(session_blobs(node_name))