changeset 72823 | ab1a49ac456b |
parent 72822 | 8d166825265e |
child 72842 | 6aae62f55c2b |
--- a/src/Pure/Tools/update.scala Sat Dec 05 13:37:37 2020 +0100 +++ b/src/Pure/Tools/update.scala Sat Dec 05 13:45:09 2020 +0100 @@ -44,7 +44,7 @@ val snapshot = args.snapshot for (node_name <- snapshot.node_files) { - val node = snapshot.version.nodes(node_name) + val node = snapshot.get_node(node_name) val xml = snapshot.state.xml_markup(snapshot.version, node_name, elements = Markup.Elements(Markup.UPDATE, Markup.LANGUAGE))