Better tooltips.

diff --git a/helm/matita/matita.glade b/helm/matita/matita.glade
index fee0d26ad8c07b2367a7ed2d2592c65739b63a92..9d90662144a6cebfe119c919b3b9e9a4b37bc15b 100644 (file)
--- a/helm/matita/matita.glade
+++ b/helm/matita/matita.glade
@@ -1928,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>
@@ -1964,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>
@@ -2035,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>
@@ -2071,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>