diff -r 005abcb34849 -r 769a7cd5a16a src/Pure/Tools/build.scala --- 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) {