From f1ead5ca7c899816e6b6ba37f13cc87eb4c4b2cf Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 20 Jul 2005 16:38:17 +0000
Subject: [PATCH] Tooltip removed.

---
 helm/matita/matita.glade | 1 -
 1 file changed, 1 deletion(-)

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>
-- 
2.39.2