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;