-
anonym authored
The current name is completely wrong -- the menu navigation was completely broken due to #11718 and it was thought we would be able to fix it and revert the GNOME Activities workaround, and just skip the renaming since the workaround was temporary. Well, it seems that the menu handling still is not reliable, even with #11718 fixed, so let's stick with what has worked pretty good during the feature/stretch development. Refs: #11718
be98070a