[gnome-shell-extensions] window-list: Update workspace names in-place

[Florian Müllner <fmuellner src gnome org>]

commit bdf6af3ee3c96855fbc9846b6580ba6f7638c47c
Author: Florian Müllner <fmuellner gnome org>
Date:   Wed Jun 5 04:57:39 2019 +0200

    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 7c0360a..9888838 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;