src/Pure/Build/build.scala
changeset 82754 6204f51104da
parent 82744 0ca8b1861fa3
child 82761 88ffadf17062
--- a/src/Pure/Build/build.scala	Tue Jun 24 22:11:04 2025 +0200
+++ b/src/Pure/Build/build.scala	Tue Jun 24 22:17:35 2025 +0200
@@ -786,8 +786,8 @@
     metric: Pretty.Metric = Symbol.Metric,
     unicode_symbols: Boolean = false
   ): Unit = {
-    val store = Store(options)
     val session = new Session(options)
+    val store = session.store
 
     def check(filter: List[Regex], make_string: => String): Boolean =
       filter.isEmpty || {