diff -r 555fb8c536b3 -r 4be047eaee2b src/Pure/Tools/build_process.scala --- a/src/Pure/Tools/build_process.scala Sat Jul 08 15:52:57 2023 +0200 +++ b/src/Pure/Tools/build_process.scala Sat Jul 08 16:07:45 2023 +0200 @@ -288,7 +288,7 @@ old_data: Map[String, A] ): Map[String, A] = { val dom = data_domain -- old_data.keysIterator - val data = old_data -- old_data.keysIterator.filterNot(dom) + val data = old_data -- old_data.keysIterator.filterNot(data_domain) if (dom.isEmpty) data else data_iterator(dom).foldLeft(data) { case (map, a) => map + (a.name -> a) } }