Files
gnome-shell-extensions/extensions
Florian Müllner 3cde65e85e window-list: Call destroy() on menus instead of their actors
PopupBaseMenu provides a destroy() method that will destroy the menu
actor and make sure that the menu will be removed from the corresponding
PopupMenuManager (if any). We miss the latter when we destroy the menu
actor directly, so use the menu method instead.

https://bugzilla.gnome.org/show_bug.cgi?id=724688
2014-02-18 21:12:16 +01:00
..