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 || {