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

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

commit d1674c5f75b5c229c5e668cdd2880117201f8dd5
Author: Florian Müllner <fmuellner gnome org>
Date:   Sun Jun 9 23:03:55 2019 +0000

    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 f443c3f..ef10d8f 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;