src/Pure/Build/build_job.scala
changeset 82750 0e36478a1b6a
parent 82744 0ca8b1861fa3
child 82752 20ffc02d0b0e
--- 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))