From d1674c5f75b5c229c5e668cdd2880117201f8dd5 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Florian=20M=C3=BCllner?= Date: Sun, 9 Jun 2019 23:03:55 +0000 Subject: [PATCH] workspace-indicator: 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/71 --- extensions/workspace-indicator/extension.js | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/extensions/workspace-indicator/extension.js b/extensions/workspace-indicator/extension.js index f443c3f4..ef10d8fe 100644 --- a/extensions/workspace-indicator/extension.js +++ b/extensions/workspace-indicator/extension.js @@ -51,7 +51,7 @@ class WorkspaceIndicator extends PanelMenu.Button { this._settings = new Gio.Settings({ schema_id: WORKSPACE_SCHEMA }); this._settingsChangedId = this._settings.connect( `changed::${WORKSPACE_KEY}`, - this._createWorkspacesSection.bind(this)); + this._updateMenuLabels.bind(this)); } _onDestroy() { @@ -82,6 +82,11 @@ class WorkspaceIndicator extends PanelMenu.Button { return Meta.prefs_get_workspace_name(workspaceIndex); } + _updateMenuLabels() { + for (let i = 0; i < this._workspacesItems.length; i++) + this._workspacesItems[i].label.text = this._labelText(i); + } + _createWorkspacesSection() { let workspaceManager = global.workspace_manager;