Comment 10 for bug 1795668

Yep: @nicolas-bernaerts is right. Ubuntu should include this commit:

https://gitlab.gnome.org/GNOME/gnome-desktop/commit/259e7e4edb0d9b84fb7cf0847149ff8d42ab9a56

since we have unmerged /usr.

Also, the problem with alternatives still stands, see https://gitlab.gnome.org/GNOME/gnome-desktop/issues/92