From ee55b3c9f43adc5adfe2c1be33bbe185aabe381c Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Wed, 13 Jul 2005 12:41:19 +0000
Subject: [PATCH] some more replace facility: alt-r

---
 helm/matita/matita.glade | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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>
-- 
2.39.2