Tooltip removed.

[helm.git] / helm / matita / matita.glade

diff --git a/helm/matita/matita.glade b/helm/matita/matita.glade
index 31faf6e08b7b21b134bd7bfe0b1c7f30272245cf..fee0d26ad8c07b2367a7ed2d2592c65739b63a92 100644 (file)
--- a/helm/matita/matita.glade
+++ b/helm/matita/matita.glade
@@ -1118,7 +1118,6 @@
                          <child>
                            <widget class="GtkCheckMenuItem" id="tacticsBarMenuItem">
                              <property name="visible">True</property>
-                             <property name="tooltip" translatable="yes">Show/Hide the tactics buttons bar</property>
                              <property name="label" translatable="yes">Show _Tactics Bar</property>
                              <property name="use_underline">True</property>
                              <property name="active">True</property>