# HG changeset patch
# User wenzelm
# Date 1353773110 -3600
# Node ID 5ab700fd512854dff47287db21e07f49b441ba84
# Parent  6d22f5a7335c4a06c0ada83978949ad217e6b86b
avoid empty tooltip;

diff -r 6d22f5a7335c -r 5ab700fd5128 src/Tools/jEdit/src/symbols_dockable.scala
--- a/src/Tools/jEdit/src/symbols_dockable.scala	Sat Nov 24 16:59:07 2012 +0100
+++ b/src/Tools/jEdit/src/symbols_dockable.scala	Sat Nov 24 17:05:10 2012 +0100
@@ -60,7 +60,7 @@
           new FlowPanel {
             contents ++= symbols.map(new Symbol_Component(_))
             if (group == "control") contents += new Reset_Component
-          })
+          }, null)
       }).toList.sortWith(_.title <= _.title)
     pages += new TabbedPane.Page("search", new BorderPanel {
       val search = new TextField(10)