src/Pure/Tools/build.scala
changeset 71971 34be842f3531
parent 71970 67fb92378224
child 71978 3e54088a7119
--- a/src/Pure/Tools/build.scala	Sat Jun 20 15:09:20 2020 +0200
+++ b/src/Pure/Tools/build.scala	Sat Jun 20 16:18:33 2020 +0200
@@ -218,7 +218,11 @@
 
         if (options.bool("pide_session")) {
           val resources = new Resources(sessions_structure, deps(parent))
-          val session = new Session(options, resources)
+          val session =
+            new Session(options, resources) {
+              override val xml_cache: XML.Cache = store.xml_cache
+              override val xz_cache: XZ.Cache = store.xz_cache
+            }
 
           val build_session_errors: Promise[List[String]] = Future.promise
           val stdout = new StringBuilder(1000)