diff -r 1629a57f3ef3 -r 0e36478a1b6a src/Pure/Build/build_job.scala --- 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))