From a7cea0ce6aac63e81420e65ac0295112252afceb Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Sat, 22 Dec 2018 00:39:03 +0100
Subject: [PATCH] GtkHSeparator deprecated

GtkSeparator used instead
---
 matita/matita/matita.ui | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/matita/matita/matita.ui b/matita/matita/matita.ui
index 1b567aef6..8a7cc1978 100644
--- a/matita/matita/matita.ui
+++ b/matita/matita/matita.ui
@@ -136,9 +136,10 @@
           </packing>
         </child>
         <child>
-          <object class="GtkHSeparator" id="hseparator3">
+          <object class="GtkSeparator" id="hseparator3">
             <property name="visible">True</property>
             <property name="can_focus">False</property>
+            <property name="orientation">horizontal</property>
           </object>
           <packing>
             <property name="expand">False</property>
-- 
2.39.2