diff -r 5d036f258f28 -r 6204f51104da src/Pure/Build/build.scala --- 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 || {