From 5b73960f34ada5e93d6cd4b670e509a0bd5248ee Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Florian=20M=C3=BCllner?= Date: Wed, 15 Apr 2020 23:32:20 +0200 Subject: [PATCH] extensions: Stop using :margin shortcut The property has been removed in GTK4, so prepare for a port by setting the four individual margin properties instead. Part-of: --- extensions/user-theme/prefs.js | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) diff --git a/extensions/user-theme/prefs.js b/extensions/user-theme/prefs.js index 241e3c98..029483ce 100644 --- a/extensions/user-theme/prefs.js +++ b/extensions/user-theme/prefs.js @@ -33,7 +33,10 @@ class UserThemePrefsWidget extends Gtk.ScrolledWindow { halign: Gtk.Align.CENTER, valign: Gtk.Align.START, hexpand: true, - margin: 60, + margin_start: 60, + margin_end: 60, + margin_top: 60, + margin_bottom: 60, }); this._list.get_style_context().add_class('frame'); this._list.set_header_func(this._updateHeader.bind(this)); @@ -141,7 +144,10 @@ class ThemeRow extends Gtk.ListBoxRow { const box = new Gtk.Box({ spacing: 12, - margin: 12, + margin_start: 12, + margin_end: 12, + margin_top: 12, + margin_bottom: 12, }); this.add(box);