changeset 75730 | 6f46853dbec4 |
parent 75727 | 5d84eec43114 |
child 75731 | 5d225d786177 |
--- a/src/Pure/Tools/build.scala Sat Jul 30 13:53:15 2022 +0200 +++ b/src/Pure/Tools/build.scala Sat Jul 30 13:58:01 2022 +0200 @@ -496,7 +496,7 @@ using(store.open_database_context()) { db_context => val presentation_nodes = - Presentation.read_nodes(presentation_sessions.map(_.name), deps, db_context) + Presentation.Nodes.read(presentation_sessions.map(_.name), deps, db_context) Par_List.map({ (session: String) => progress.expose_interrupt()