author | wenzelm |
Sat, 11 Mar 2023 11:14:24 +0100 | |
changeset 77604 | b4ef44ce08ed |
parent 77603 | 236e43c8bb5b |
child 77605 | bc1248c5d159 |
--- a/src/Pure/Tools/build_process.scala Sat Mar 11 11:13:53 2023 +0100 +++ b/src/Pure/Tools/build_process.scala Sat Mar 11 11:14:24 2023 +0100 @@ -923,7 +923,7 @@ final def start_build(): Unit = synchronized_database { for (db <- _database) { Build_Process.Data.start_build(db, build_uuid, build_context.ml_platform, - store.options.make_prefs(Options.init(prefs = ""))) + store.options.make_prefs(Options.init(prefs = ""), filter = _.is_exported)) } }