changeset 82744 | 0ca8b1861fa3 |
parent 82742 | 085e624a1303 |
child 82754 | 6204f51104da |
--- a/src/Pure/Build/build.scala Mon Jun 23 14:44:59 2025 +0200 +++ b/src/Pure/Build/build.scala Tue Jun 24 20:52:09 2025 +0200 @@ -787,7 +787,7 @@ unicode_symbols: Boolean = false ): Unit = { val store = Store(options) - val session = new Session(options, Resources.bootstrap) + val session = new Session(options) def check(filter: List[Regex], make_string: => String): Boolean = filter.isEmpty || {