From 3bb0897bc1b90bf522b77a225c7eeb419fbb9926 Mon Sep 17 00:00:00 2001 From: Adam Goode Date: Sat, 8 May 2021 11:49:56 -0400 Subject: [PATCH] window-list: Don't use panel-button class for the workspace indicator The panel-button introduces some horizontal padding which is insensitive to scroll events. Without this change, there is a small dead zone in the corner that cannot be used to switch workspaces with the mouse wheel. For useMenu mode, this has the effect of removing all of the horizontal space to the edge of the screen, so I add some back with the status-label-bin margin. This a is similar change to 8bad8a3b63d8719163dd0fb7fc9b2fd67969931c. Fixes #315. Part-of: (cherry picked from commit d6648b0b5c2a27c5ffaf2dcd353afacf3e8dd538) --- extensions/window-list/stylesheet.css | 2 +- extensions/window-list/workspaceIndicator.js | 1 + 2 files changed, 2 insertions(+), 1 deletion(-) diff --git a/extensions/window-list/stylesheet.css b/extensions/window-list/stylesheet.css index 38ea9d86..87813a42 100644 --- a/extensions/window-list/stylesheet.css +++ b/extensions/window-list/stylesheet.css @@ -82,7 +82,7 @@ background-color: rgba(200, 200, 200, .3); border: 1px solid #cccccc; padding: 0 3px; - margin: 3px 0; + margin: 3px; } .window-list-workspace-indicator .workspaces-box { diff --git a/extensions/window-list/workspaceIndicator.js b/extensions/window-list/workspaceIndicator.js index 41eedf63..c35e37a7 100644 --- a/extensions/window-list/workspaceIndicator.js +++ b/extensions/window-list/workspaceIndicator.js @@ -249,6 +249,7 @@ class WorkspaceIndicator extends PanelMenu.Button { super._init(0.0, _('Workspace Indicator'), true); this.setMenu(new PopupMenu.PopupMenu(this, 0.0, St.Side.BOTTOM)); this.add_style_class_name('window-list-workspace-indicator'); + this.remove_style_class_name('panel-button'); this.menu.actor.remove_style_class_name('panel-menu'); let container = new St.Widget({