From dc861d214cb992a898f81752614201b8074eef12 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 20 Jul 2005 16:41:31 +0000
Subject: [PATCH] Better tooltips.

---
 helm/matita/matita.glade | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

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