changeset 75394 | 42267c650205 |
parent 75393 | 87ebf5a50283 |
child 82142 | 508a673c87ac |
--- a/src/Tools/Graphview/mutator.scala Fri Apr 01 17:06:10 2022 +0200 +++ b/src/Tools/Graphview/mutator.scala Fri Apr 01 23:19:12 2022 +0200 @@ -152,7 +152,7 @@ extends Graph_Mutator( "Add transitive closure", "Adds all family members of all current nodes.", - (full_graph, graph) => { + { (full_graph, graph) => val withparents = if (parents) add_node_group(full_graph, graph, full_graph.all_preds(graph.keys)) else graph