From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 20 Jul 2005 16:41:31 +0000 (+0000)
Subject: Better tooltips.
X-Git-Tag: V_0_7_2~133
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=dc861d214cb992a898f81752614201b8074eef12;p=helm.git

Better tooltips.
---

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>