60e386048b
The animation was removed in commit 6a00a504d4fc for consistency with other menus. However commit a9b12d5d737dc then *added* animations to those just four minutes later. So add back the original animations for consistency, both with menu closing and with other menus. https://gitlab.gnome.org/GNOME/gnome-shell/issues/1595