Add a new tool, 'gnome-shell-extension-prefs', which can configure extensions

A new tool, 'gnome-shell-extension-prefs' can load a new entry point from
extensions, 'prefs.js', which has an entry point to return a GTK+ widget.
This allows extensions to have their own preferences dialog, without each
extension needing to ship its own Python script and .desktop file.

https://bugzilla.gnome.org/show_bug.cgi?id=668429
This commit is contained in:
Jasper St. Pierre 2012-01-18 21:21:56 -05:00
parent 80ff6ff797
commit b8a54faf94
8 changed files with 326 additions and 4 deletions

3
.gitignore vendored
View file

@ -18,6 +18,8 @@ config
configure
data/gnome-shell.desktop
data/gnome-shell.desktop.in
data/gnome-shell-extension-prefs.desktop
data/gnome-shell-extension-prefs.desktop.in
data/gschemas.compiled
data/org.gnome.shell.gschema.xml
data/org.gnome.shell.gschema.valid
@ -62,6 +64,7 @@ src/calendar-server/org.gnome.Shell.CalendarServer.service
src/gnome-shell
src/gnome-shell-calendar-server
src/gnome-shell-extension-tool
src/gnome-shell-extension-prefs
src/gnome-shell-hotplug-sniffer
src/gnome-shell-jhbuild
src/gnome-shell-perf-helper