# HG changeset patch
# User wenzelm
# Date 1420293273 -3600
# Node ID 21ef04bd4e17057a026c7b3e51f7a01d21673559
# Parent  fda4091cc6b0f82e5d7e2d1e8f01834d2aa16839
recovered tooltip from 6e77ddb1e3fb: non-null default is required as prerequisite;

diff -r fda4091cc6b0 -r 21ef04bd4e17 src/Tools/Graphview/graph_panel.scala
--- 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 {