| changeset 71601 | 97ccf48c2f0c |
| parent 67547 | aefe7a7b330a |
| child 73340 | 0ffcad1f6130 |
--- a/src/Tools/Graphview/graphview.scala Fri Mar 27 13:04:15 2020 +0100 +++ b/src/Tools/Graphview/graphview.scala Fri Mar 27 22:01:27 2020 +0100 @@ -82,7 +82,7 @@ } else node.toString - _layout = Layout.make(options, metrics, node_text _, visible_graph) + _layout = Layout.make(options, metrics, node_text, visible_graph) }