added autosave and * (modified feature)

[helm.git] / helm / matita / matita.glade

diff --git a/helm/matita/matita.glade b/helm/matita/matita.glade
index 47d8a3d1e1f693422169de66393a058af9338987..98526c5788d2a1ef51600a7e7880313980a5844c 100644 (file)
--- a/helm/matita/matita.glade
+++ b/helm/matita/matita.glade
@@ -1970,7 +1970,7 @@ Copyright (C) 2005,
                              </child>
 
                              <child>
-                               <widget class="GtkLabel" id="label12">
+                               <widget class="GtkLabel" id="scriptLabel">
                                  <property name="visible">True</property>
                                  <property name="label" translatable="yes">script</property>
                                  <property name="use_underline">False</property>