Florian Müllner 8795668c41 extensionPrefs: Rename to Extensions ...

... and make the application user-visible.

https://gitlab.gnome.org/GNOME/gnome-shell/issues/1968

2020-02-03 19:03:19 +01:00

..

ui

extensionPrefs: Rename to Extensions

2020-02-03 19:03:19 +01:00

main.js

extensionPrefs: Rename to Extensions

2020-02-03 19:03:19 +01:00