From bdf6af3ee3c96855fbc9846b6580ba6f7638c47c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Florian=20M=C3=BCllner?= Date: Wed, 5 Jun 2019 04:57:39 +0200 Subject: [PATCH] window-list: Update workspace names in-place There's no good reason to rebuild the entire menu on workspace names changes, we can simply update the labels in-place. https://gitlab.gnome.org/GNOME/gnome-shell-extensions/merge_requests/70 --- extensions/window-list/workspaceIndicator.js | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/extensions/window-list/workspaceIndicator.js b/extensions/window-list/workspaceIndicator.js index 7c0360a2..98888384 100644 --- a/extensions/window-list/workspaceIndicator.js +++ b/extensions/window-list/workspaceIndicator.js @@ -47,7 +47,7 @@ var WorkspaceIndicator = GObject.registerClass({ this._settings = new Gio.Settings({ schema_id: 'org.gnome.desktop.wm.preferences' }); this._settingsChangedId = this._settings.connect( - 'changed::workspace-names', this._updateMenu.bind(this)); + 'changed::workspace-names', this._updateMenuLabels.bind(this)); } _onDestroy() { @@ -78,6 +78,14 @@ var WorkspaceIndicator = GObject.registerClass({ return '%d / %d'.format(current + 1, total); } + _updateMenuLabels() { + for (let i = 0; i < this._workspacesItems.length; i++) { + let item = this._workspacesItems[i]; + let name = Meta.prefs_get_workspace_name(i); + item.label.text = name; + } + } + _updateMenu() { let workspaceManager = global.workspace_manager;