-
Florian Müllner authored
The gnome-extensions tool[0] was started as an external project, and provides a replacement for the existing gnome-shell-extension-tool. It was decided to ship the tool as part of the gnome-shell repository, so start importing it with its history into a subdir. [0] https://gitlab.gnome.org/fmuellner/gnome-extensions-tool GNOME/gnome-shell#1234
d8c7cac5