From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 20 Jul 2005 16:38:17 +0000 (+0000)
Subject: Tooltip removed.
X-Git-Tag: V_0_7_2~134
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f1ead5ca7c899816e6b6ba37f13cc87eb4c4b2cf;p=helm.git

Tooltip removed.
---

diff --git a/helm/matita/matita.glade b/helm/matita/matita.glade
index 31faf6e08..fee0d26ad 100644
--- 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>