Commit dbb71f0d authored by Florian Müllner's avatar Florian Müllner

layout: Make the hot corner optional

Whether people love or hate the hot corner depends in large extents
on hardware sensitivity and habits, which is hard to get right
universally. So bite the bullet and support an option to enable or
disable hot corners ...

https://bugzilla.gnome.org/show_bug.cgi?id=688320
parent 1cac7b22
Pipeline #94264 passed with stages
in 5 minutes and 11 seconds
// -*- mode: js; js-indent-level: 4; indent-tabs-mode: nil -*-
const { Clutter, GLib, GObject, Meta, Shell, St } = imports.gi;
const { Clutter, Gio, GLib, GObject, Meta, Shell, St } = imports.gi;
const Signals = imports.signals;
const Background = imports.ui.background;
......@@ -274,6 +274,13 @@ var LayoutManager = GObject.registerClass({
this._backgroundGroup.lower_bottom();
this._bgManagers = [];
this._interfaceSettings = new Gio.Settings({
schema_id: 'org.gnome.desktop.interface'
});
this._interfaceSettings.connect('changed::enable-hot-corners',
this._updateHotCorners.bind(this));
// Need to update struts on new workspaces when they are added
let workspaceManager = global.workspace_manager;
workspaceManager.connect('notify::n-workspaces',
......@@ -377,6 +384,11 @@ var LayoutManager = GObject.registerClass({
});
this.hotCorners = [];
if (!this._interfaceSettings.get_boolean('enable-hot-corners')) {
this.emit('hot-corners-changed');
return;
}
let size = this.panelBox.height;
// build new hot corners
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment