changeset 82780 | beba766806ed |
parent 82761 | 88ffadf17062 |
child 82784 | 0751d363fd0e |
--- a/src/Pure/Build/build.scala Fri Jun 27 13:44:36 2025 +0200 +++ b/src/Pure/Build/build.scala Fri Jun 27 14:41:18 2025 +0200 @@ -786,7 +786,7 @@ metric: Pretty.Metric = Symbol.Metric, unicode_symbols: Boolean = false ): Unit = { - val session = new Session(options) + val session = new Session { override def session_options: Options = options } val store = session.store def check(filter: List[Regex], make_string: => String): Boolean =