pool/gnome-shell-extensions
SHA256
2
0
Fork 1
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Accepting request 627475 from GNOME:Factory

Browse Source 
OBS-URL: https://build.opensuse.org/request/show/627475
OBS-URL: https://build.opensuse.org/package/show/openSUSE:Factory/gnome-shell-extensions?expand=0&rev=84
This commit is contained in:
Dominique Leuenberger 2018-08-07 07:42:07 +00:00 committed by Git OBS Bridge
commit 34835c9dfa
2 changed files with 38 additions and 9 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

9
gnome-shell-extensions.changes
View File

@ -1,3 +1,12 @@
-------------------------------------------------------------------
Fri Aug 3 06:05:03 UTC 2018 - qkzhu@suse.com
- Update gse-sle-classic-ext.patch CSS files are generated by Sass
sources in 3.28, the default margin-bottom of popup-menu.panel-menu
is 1.75em which creates an ugly gap between menu and its source
actor when the PanelMenu's source actor is at the bottom
(boo#1094148).
-------------------------------------------------------------------
Tue Jul 24 16:52:54 UTC 2018 - dimstar@opensuse.org

38
gse-sle-classic-ext.patch
View File

@ -1,7 +1,7 @@
Index: gnome-shell-extensions-3.27.91/extensions/window-list/classic.css
Index: gnome-shell-extensions-3.28.1+20180413.6746061/extensions/window-list/classic.css
===================================================================
--- gnome-shell-extensions-3.27.91.orig/extensions/window-list/classic.css
+++ gnome-shell-extensions-3.27.91/extensions/window-list/classic.css
--- gnome-shell-extensions-3.28.1+20180413.6746061.orig/extensions/window-list/classic.css
+++ gnome-shell-extensions-3.28.1+20180413.6746061/extensions/window-list/classic.css
@@ -6,7 +6,7 @@
height: 2.25em ;
}
@ -43,10 +43,10 @@ Index: gnome-shell-extensions-3.27.91/extensions/window-list/classic.css
color: #888;
box-shadow: inset -1px -1px 1px rgba(0,0,0,0.5);
}
Index: gnome-shell-extensions-3.27.91/extensions/window-list/extension.js
Index: gnome-shell-extensions-3.28.1+20180413.6746061/extensions/window-list/extension.js
===================================================================
--- gnome-shell-extensions-3.27.91.orig/extensions/window-list/extension.js
+++ gnome-shell-extensions-3.27.91/extensions/window-list/extension.js
--- gnome-shell-extensions-3.28.1+20180413.6746061.orig/extensions/window-list/extension.js
+++ gnome-shell-extensions-3.28.1+20180413.6746061/extensions/window-list/extension.js
@@ -27,6 +27,395 @@ const GroupingMode = {
ALWAYS: 2
};
@ -455,10 +455,10 @@ Index: gnome-shell-extensions-3.27.91/extensions/window-list/extension.js
+ return new Extension();
+ }
}
Index: gnome-shell-extensions-3.27.91/extensions/window-list/stylesheet.css
Index: gnome-shell-extensions-3.28.1+20180413.6746061/extensions/window-list/stylesheet.css
===================================================================
--- gnome-shell-extensions-3.27.91.orig/extensions/window-list/stylesheet.css
+++ gnome-shell-extensions-3.27.91/extensions/window-list/stylesheet.css
--- gnome-shell-extensions-3.28.1+20180413.6746061.orig/extensions/window-list/stylesheet.css
+++ gnome-shell-extensions-3.28.1+20180413.6746061/extensions/window-list/stylesheet.css
@@ -79,6 +79,10 @@
border: 1px solid #cccccc;
}
@ -470,3 +470,23 @@ Index: gnome-shell-extensions-3.27.91/extensions/window-list/stylesheet.css
.notification {
font-weight: normal;
}
Index: gnome-shell-extensions-3.28.1+20180413.6746061/data/gnome-classic.scss
===================================================================
--- gnome-shell-extensions-3.28.1+20180413.6746061.orig/data/gnome-classic.scss
+++ gnome-shell-extensions-3.28.1+20180413.6746061/data/gnome-classic.scss
@@ -103,3 +103,15 @@ $variant: 'light';
&:hover, &focus { background-color: darken($bg_color,2%); }
}
}
+
+.popup-menu {
+ &.panel-menu {
+ -boxpointer-gap: 4px;
+ /* TODO was 1.75em, no idea of its use */
+ /* NOTE: the following creates an ugly gap between menu and its source actor
+ when the PanelMenu's source actor is at the bottom. Preferrably for
+ bottom menu, `margin-top` might be a better choice. However, since we
+ have no idea about its use so reset to 0 for now. */
+ margin-bottom: 0em;
+ }
+}