src/Pure/Tools/build.scala
changeset 76206 769a7cd5a16a
parent 76202 d535db35388e
child 76209 365f6a621fc5
--- a/src/Pure/Tools/build.scala	Thu Sep 22 20:04:57 2022 +0200
+++ b/src/Pure/Tools/build.scala	Thu Sep 22 20:20:37 2022 +0200
@@ -137,9 +137,12 @@
   /** build with results **/
 
   class Results private[Build](
+    val store: Sessions.Store,
     results: Map[String, (Option[Process_Result], Sessions.Info)],
     val presentation_sessions: List[String]
   ) {
+    def cache: Term.Cache = store.cache
+
     def sessions: Set[String] = results.keySet
     def cancelled(name: String): Boolean = results(name)._1.isEmpty
     def info(name: String): Sessions.Info = results(name)._2
@@ -461,7 +464,7 @@
           if result.ok && browser_info.enabled(result.info)
         } yield name).toList
 
-      new Results(results, presentation_sessions)
+      new Results(store, results, presentation_sessions)
     }
 
     if (export_files) {