[gnome-shell-extensions] workspace-indicator: Adjust to PopupMenu API change

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

commit 8ba3bedd20b62549e2302d172695cad9630fcb3a
Author: Florian Müllner <fmuellner gnome org>
Date:   Tue Apr 30 17:16:25 2013 +0200

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

 extensions/workspace-indicator/extension.js |    6 +++---
 1 files changed, 3 insertions(+), 3 deletions(-)
---
diff --git a/extensions/workspace-indicator/extension.js b/extensions/workspace-indicator/extension.js
index c07152b..7f65324 100644
--- a/extensions/workspace-indicator/extension.js
+++ b/extensions/workspace-indicator/extension.js
@@ -66,9 +66,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._labelText());
     },
@@ -98,7 +98,7 @@ const WorkspaceIndicator = new Lang.Class({
            }));
 
            if (i == this._currentWorkspace)
-               this.workspacesItems[i].setShowDot(true);
+               this.workspacesItems[i].setOrnament(PopupMenu.Ornament.DOT);
        }
 
        this.statusLabel.set_text(this._labelText());