author | wenzelm |
Sun, 18 Jan 2015 22:22:12 +0100 | |
changeset 59401 | 6ee01e011976 |
parent 59400 | d833cba5cce5 |
child 59402 | 4de91de47a6c |
--- a/src/Tools/Graphview/visualizer.scala Sun Jan 18 22:20:48 2015 +0100 +++ b/src/Tools/Graphview/visualizer.scala Sun Jan 18 22:22:12 2015 +0100 @@ -79,7 +79,6 @@ } else node.toString - // FIXME avoid expensive operation on GUI thread _layout = Layout.make(options, metrics, node_text _, visible_graph) }