Skip to content

Import gnome-extensions tool

Florian Müllner requested to merge fmuellner/gnome-shell:extension-tool into master

gnome-extensions is a small tool I wrote a while ago as a more useful replacement for gnome-shell-extensions-tool. Feedback in #1234 (closed) was generally in favor of shipping it with gnome-shell itself, so this is importing its sources and history.

Resolves #1234 (closed)

Merge request reports