[gnome-shell-extensions] window-list: Adjust to PopupMenu API change

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

commit 8628addfc9c69e0cca4020e1a69bb757f7d25cff
Author: Florian Müllner <fmuellner gnome org>
Date:   Tue Apr 30 17:14:07 2013 +0200

    window-list: Adjust to PopupMenu API change
    
    setShowDot() has become setOrnament().
    
    https://bugzilla.gnome.org/show_bug.cgi?id=699335

 extensions/window-list/extension.js |    6 +++---
 1 files changed, 3 insertions(+), 3 deletions(-)
---
diff --git a/extensions/window-list/extension.js b/extensions/window-list/extension.js
index 93f9456..425d1c8 100644
--- a/extensions/window-list/extension.js
+++ b/extensions/window-list/extension.js
@@ -414,9 +414,9 @@ const WorkspaceIndicator = new Lang.Class({
     },
 
     _updateIndicator: function() {
-        this.workspacesItems[this._currentWorkspace].setShowDot(false);
+        this.workspacesItems[this._currentWorkspace].setOrnament(PopupMenu.Ornament.NONE);
         this._currentWorkspace = global.screen.get_active_workspace().index();
-        this.workspacesItems[this._currentWorkspace].setShowDot(true);
+        this.workspacesItems[this._currentWorkspace].setOrnament(PopupMenu.Ornament.DOT);
 
         this.statusLabel.set_text(this._getStatusText());
     },
@@ -443,7 +443,7 @@ const WorkspaceIndicator = new Lang.Class({
             }));
 
             if (i == this._currentWorkspace)
-                item.setShowDot(true);
+                item.setOrnament(PopupMenu.Ornament.DOT);
 
             this.menu.addMenuItem(item);
             this.workspacesItems[i] = item;