[gnome-continuous] Fix config-opts for gnome-shell

[Emmanuele Bassi <ebassi src gnome org>]

commit 1e3c38d35be50cf733552d3bfa834c4e6247a139
Author: Emmanuele Bassi <ebassi gnome org>
Date:   Fri Dec 1 01:38:30 2017 +0000

    Fix config-opts for gnome-shell
    
    The configuration options were renamed.

 manifest.json |    6 +++---
 1 files changed, 3 insertions(+), 3 deletions(-)
---
diff --git a/manifest.json b/manifest.json
index bd3a8e4..868d2d4 100644
--- a/manifest.json
+++ b/manifest.json
@@ -1112,9 +1112,9 @@
                {"src": "gnome:gnome-shell",
                  "patches": ["gnome-shell-gir-hack.patch"],
                  "irc_room": "gnome-shell",
-                "config-opts": ["-Denable-documentation=false",
-                                 "-Denable-man=false",
-                                 "-Denable-browser-plugin=false"]},
+                "config-opts": ["-Dgtk_doc=false",
+                                 "-Dman=false",
+                                 "-Dbrowser_plugin=false"]},
 
                {"src": "gnome-gitlab:GNOME/gnome-shell-extensions.git",
                 "config-opts": ["--enable-extensions=classic-mode"]},