isa/gnome-shell
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

extensions-app: Stop using :margin shortcut

Browse Source 
The property has been removed in GTK4, so prepare for a port by
setting the four individual margin properties instead.

Part-of: <https://gitlab.gnome.org/GNOME/gnome-shell/-/merge_requests/1495>
This commit is contained in:
Florian Müllner
2020-04-15 20:27:15 +02:00
committed by Marge Bot
parent ad6fbaa245
commit 3af90918a3
3 changed files with 28 additions and 7 deletions
Download Patch File Download Diff File Expand all files Collapse all files

10
subprojects/extensions-app/js/main.js
View File

@ -152,7 +152,10 @@ var ExtensionsWindow = GObject.registerClass({
this._userList.set_filter_func(this._filterList.bind(this));
this._userList.set_placeholder(new Gtk.Label({
label: _('No Matches'),
margin: 12,
margin_start: 12,
margin_end: 12,
margin_top: 12,
margin_bottom: 12,
visible: true,
}));
@ -161,7 +164,10 @@ var ExtensionsWindow = GObject.registerClass({
this._systemList.set_filter_func(this._filterList.bind(this));
this._systemList.set_placeholder(new Gtk.Label({
label: _('No Matches'),
margin: 12,
margin_start: 12,
margin_end: 12,
margin_top: 12,
margin_bottom: 12,
visible: true,
}));