MatitaSync.remove must remove the objects also from the environment.

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

diff --git a/helm/matita/matita.glade b/helm/matita/matita.glade
index 31faf6e08b7b21b134bd7bfe0b1c7f30272245cf..9d90662144a6cebfe119c919b3b9e9a4b37bc15b 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>
@@ -1929,7 +1928,7 @@
                                  <child>
                                    <widget class="GtkButton" id="scriptTopButton">
                                      <property name="visible">True</property>
-                                     <property name="tooltip" translatable="yes">restart (Home)</property>
+                                     <property name="tooltip" translatable="yes">restart (Ctrl+Home)</property>
                                      <property name="can_focus">True</property>
                                      <property name="relief">GTK_RELIEF_NONE</property>
                                      <property name="focus_on_click">True</property>
@@ -1965,7 +1964,7 @@
                                  <child>
                                    <widget class="GtkButton" id="scriptRetractButton">
                                      <property name="visible">True</property>
-                                     <property name="tooltip" translatable="yes">go back 1 phrase (Page Up)</property>
+                                     <property name="tooltip" translatable="yes">go back 1 phrase (Ctrl+Page Up)</property>
                                      <property name="can_focus">True</property>
                                      <property name="relief">GTK_RELIEF_NONE</property>
                                      <property name="focus_on_click">True</property>
@@ -2036,7 +2035,7 @@
                                  <child>
                                    <widget class="GtkButton" id="scriptAdvanceButton">
                                      <property name="visible">True</property>
-                                     <property name="tooltip" translatable="yes">go forward 1 phrase (Page Down)</property>
+                                     <property name="tooltip" translatable="yes">go forward 1 phrase (Ctrl+Page Down)</property>
                                      <property name="can_focus">True</property>
                                      <property name="relief">GTK_RELIEF_NONE</property>
                                      <property name="focus_on_click">True</property>
@@ -2072,7 +2071,7 @@
                                  <child>
                                    <widget class="GtkButton" id="scriptBottomButton">
                                      <property name="visible">True</property>
-                                     <property name="tooltip" translatable="yes">execute all (End)</property>
+                                     <property name="tooltip" translatable="yes">execute all (Ctrl+End)</property>
                                      <property name="can_focus">True</property>
                                      <property name="relief">GTK_RELIEF_NONE</property>
                                      <property name="focus_on_click">True</property>