some more replace facility: alt-r

diff --git a/helm/matita/matita.glade b/helm/matita/matita.glade
index 10fb0a1cc84ef9a3fcb83a04e5544455eae96f75..4f77603adc88fbdc86d000114e30a39f88af6d39 100644 (file)
--- 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>