changeset 82784 | 0751d363fd0e |
parent 82780 | beba766806ed |
child 82793 | fe8598c92be7 |
--- a/src/Pure/Build/build.scala Fri Jun 27 14:52:01 2025 +0200 +++ b/src/Pure/Build/build.scala Fri Jun 27 15:03:12 2025 +0200 @@ -786,7 +786,7 @@ metric: Pretty.Metric = Symbol.Metric, unicode_symbols: Boolean = false ): Unit = { - val session = new Session { override def session_options: Options = options } + val session = Session.bootstrap(options) val store = session.store def check(filter: List[Regex], make_string: => String): Boolean =