From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Wed, 13 Jul 2005 12:41:19 +0000 (+0000)
Subject: some more replace facility: alt-r
X-Git-Tag: pre_notation~17
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=ee55b3c9f43adc5adfe2c1be33bbe185aabe381c;p=helm.git

some more replace facility: alt-r
---

diff --git a/helm/matita/matita.glade b/helm/matita/matita.glade
index 10fb0a1cc..4f77603ad 100644
--- a/helm/matita/matita.glade
+++ b/helm/matita/matita.glade
@@ -2972,7 +2972,7 @@ Copyright (C) 2005,
 		      <child>
 			<widget class="GtkLabel" id="label19">
 			  <property name="visible">True</property>
-			  <property name="label">Replace</property>
+			  <property name="label">_Replace</property>
 			  <property name="use_underline">True</property>
 			  <property name="use_markup">False</property>
 			  <property name="justify">GTK_JUSTIFY_LEFT</property>