author | wenzelm |
Sat, 03 Jan 2015 14:54:33 +0100 | |
changeset 59243 | 21ef04bd4e17 |
parent 59242 | fda4091cc6b0 |
child 59244 | 19b5fc4b2b38 |
--- a/src/Tools/Graphview/graph_panel.scala Sat Jan 03 14:29:07 2015 +0100 +++ b/src/Tools/Graphview/graph_panel.scala Sat Jan 03 14:54:33 2015 +0100 @@ -23,6 +23,8 @@ { panel => + tooltip = "" + override lazy val peer: JScrollPane = new JScrollPane with SuperMixin { override def getToolTipText(event: java.awt.event.MouseEvent): String = node(Transform.pane_to_graph_coordinates(event.getPoint)) match {