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