delete GLUI does nothing

[josch]

https://sourceforge.net/p/glui/bugs/12/

GLUI, GLUI_Main, GLUI_Panel, etc all have trivial
destructors.
GLUI::close() calls GLUI_Main::close_internal(), which
calls delete this->main_panel and delete this, but
neither of those two calls actually does much. None of
the controls in the GLUI window get cleaned up.