# HG changeset patch
# User wenzelm
# Date 1421616132 -3600
# Node ID 6ee01e0119768ec84abd4fcee7aba05a48ab211c
# Parent  d833cba5cce5309fc6098c6b6efa922b0269b67a
obsolete -- full layout takes approx. 100ms;

diff -r d833cba5cce5 -r 6ee01e011976 src/Tools/Graphview/visualizer.scala
--- 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)
   }