diff --git a/extensions/windowsNavigator/extension.js b/extensions/windowsNavigator/extension.js index c42d9661..3191d7ca 100644 --- a/extensions/windowsNavigator/extension.js +++ b/extensions/windowsNavigator/extension.js @@ -127,15 +127,21 @@ function enable() { workViewInjections['_hideWorkspacesTooltips'] = undefined; WorkspacesView.WorkspacesView.prototype._onKeyRelease = function(s, o) { - if (this._pickWindow && o.get_key_symbol() == Clutter.KEY_Alt_L) + if (this._pickWindow && + (o.get_key_symbol() == Clutter.KEY_Alt_L || + o.get_key_symbol() == Clutter.KEY_Alt_R)) this._hideTooltips(); - if (this._pickWorkspace && o.get_key_symbol() == Clutter.KEY_Control_L) + if (this._pickWorkspace && + (o.get_key_symbol() == Clutter.KEY_Control_L || + o.get_key_symbol() == Clutter.KEY_Control_R)) this._hideWorkspacesTooltips(); } workViewInjections['_onKeyRelease'] = undefined; WorkspacesView.WorkspacesView.prototype._onKeyPress = function(s, o) { - if (o.get_key_symbol() == Clutter.KEY_Alt_L && !this._pickWorkspace) { + if ((o.get_key_symbol() == Clutter.KEY_Alt_L || + o.get_key_symbol() == Clutter.KEY_Alt_R) + && !this._pickWorkspace) { this._prevFocusActor = global.stage.get_key_focus(); global.stage.set_key_focus(null); this._active = global.screen.get_active_workspace_index(); @@ -143,7 +149,9 @@ function enable() { this._workspaces[global.screen.get_active_workspace_index()].showWindowsTooltips(); return true; } - if (o.get_key_symbol() == Clutter.KEY_Control_L && !this._pickWindow) { + if ((o.get_key_symbol() == Clutter.KEY_Control_L || + o.get_key_symbol() == Clutter.KEY_Control_R) + && !this._pickWindow) { this._prevFocusActor = global.stage.get_key_focus(); global.stage.set_key_focus(null); this._pickWorkspace = true; @@ -155,6 +163,12 @@ function enable() { if (global.stage.get_key_focus() != global.stage) return false; + // ignore shift presses, they're required to get numerals in azerty keyboards + if ((this._pickWindow || this._pickWorkspace) && + (o.get_key_symbol() == Clutter.KEY_Shift_L || + o.get_key_symbol() == Clutter.KEY_Shift_R)) + return true; + if (this._pickWindow) { if (this._active != global.screen.get_active_workspace_index()) { this._hideTooltips(); @@ -280,4 +294,4 @@ function disable() { function init() { /* do nothing */ -} \ No newline at end of file +}