From 9a1d57694c9dd3d294d534f69268fccf5b0638d2 Mon Sep 17 00:00:00 2001
From: Wolfgang Müller
Date: Fri, 18 Jun 2021 12:26:06 +0200
Subject: terminal.ui: Stop using 'margin-left' and 'margin-right' properties

These were deprecated in GTK 3.12 [1]. Instead use 'margin-start' and
'margin-end' for the same effect.

[1] https://developer.gnome.org/gtk3/stable/GtkWidget.html#GtkWidget--margin-left
---
 terminal.ui | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/terminal.ui b/terminal.ui
index 268ee0c..3fd1ac8 100644
--- a/terminal.ui
+++ b/terminal.ui
@@ -161,8 +161,8 @@
           <object class="GtkBox" id="search_container">
             <property name="visible">True</property>
             <property name="can-focus">False</property>
-            <property name="margin-left">5</property>
-            <property name="margin-right">5</property>
+            <property name="margin-start">5</property>
+            <property name="margin-end">5</property>
             <property name="margin-top">5</property>
             <property name="margin-bottom">5</property>
             <property name="spacing">2</property>
-- 
cgit v1.2.3-2-gb3c3