set_usermenu_state 2064 core/gui.c         void set_usermenu_state();
set_usermenu_state 2065 core/gui.c         set_usermenu_state();
set_usermenu_state 2481 core/gui.c         set_usermenu_state();