46c210c314
The actual changes to shell-menu.[ch] are pretty minimal; most of the changes there are just style/spacing/indentation. Also, removed shell_menu_append_separator() since it wasn't needed; the separators would already have been behaving as intended just because they were non-reactive. https://bugzilla.gnome.org/show_bug.cgi?id=614516