As I have learned from @vanadium's answer, the app is called
Trying out Ubuntu in a live USB session, the app was not present initially.
After adding the
Universe source, I have run
sudo apt install gnome-shell-extensions --dry-run and
sudo apt install gnome-tweaks --dry-run.
I found that
gnome-shell-extension-prefs has shown up among the packages that will be installed in both the case of installing
gnome-tweaks and installing
gnome-shell-extensions. (As @vanadium has pointed out, it is because apt is configured by default to install recommended packages.)
From this, it seems safe to assume that anyone who has Gnome Tweaks installed, has the Extensions app too.
Which is all the more weird, because as I have found, Extensions can override Tweaks, and at that, without any hint: settings in Tweaks will simply not take effect, if they conflict with settings in Extensions.
Just a detail:
I remember, in the beginning (when I did not have yet
gnome-shell-extensions), being able to enable/disable the Desktop Icons extension with Tweaks.
It was only later, at some point in time, that (re-)enabling Desktop Icons became impossible through Tweaks. (Because then it had to be done with Extensions.)
Between these two experiences, I'm aware of two things happening:
- I have installed the
- I was experimenting with a
gnome-shell --replace command, which has disabled all my extensions, and each had to be re-enabled by hand.
Somehow I still think that with the above, I have disqualified myself from reliably assuming how other people's shell extension preferences work...