From 0c3f71d94db498cbefceb2dafb599bb3f6fd2957 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Tor=20Hedin=20Br=C3=B8nner?= Date: Fri, 28 Feb 2020 00:55:09 +0100 Subject: [PATCH] selection highlight: add rounded border --- navigator.js | 1 + stylesheet.css | 4 ++++ tiling.js | 2 +- 3 files changed, 6 insertions(+), 1 deletion(-) diff --git a/navigator.js b/navigator.js index ea0bb13..5c7bf1e 100644 --- a/navigator.js +++ b/navigator.js @@ -64,6 +64,7 @@ var ActionDispatcher = class { show(backward, binding, mask) { this._modifierMask = SwitcherPopup.primaryModifier(mask); this.navigator = getNavigator(); + TopBar.fixTopBar(); let actionId = Keybindings.idOf(binding); if(actionId === Meta.KeyBindingAction.NONE) { try { diff --git a/stylesheet.css b/stylesheet.css index 9873656..661a605 100644 --- a/stylesheet.css +++ b/stylesheet.css @@ -14,3 +14,7 @@ .workspace-icon-button StIcon { icon-size: 16px; } + +.paperwm-selection { + border-radius: 8px; +} diff --git a/tiling.js b/tiling.js index ad1ed57..acb9d9e 100644 --- a/tiling.js +++ b/tiling.js @@ -153,7 +153,7 @@ class Space extends Array { label.hide(); let selection = new St.Widget({name: 'selection', - style_class: 'tile-preview'}); + style_class: 'paperwm-selection tile-preview'}); this.selection = selection; clip.space = this;