building/cleaning a devel now makes buttons insensitive

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

diff --git a/helm/matita/matita.glade b/helm/matita/matita.glade
index 9d90662144a6cebfe119c919b3b9e9a4b37bc15b..a99cb2db11ccbe96b57a1267d2b340f585981571 100644 (file)
--- a/helm/matita/matita.glade
+++ b/helm/matita/matita.glade
@@ -3451,7 +3451,7 @@
       </child>
 
       <child>
-       <widget class="GtkHBox" id="hbox22">
+       <widget class="GtkHBox" id="buttonsHbox">
          <property name="border_width">3</property>
          <property name="visible">True</property>
          <property name="homogeneous">False</property>