src/Pure/Build/build.scala
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 =