--- a/ui/gtk/menu.c Sun Nov 17 15:21:50 2024 +0100 +++ b/ui/gtk/menu.c Thu Nov 21 12:04:53 2024 +0100 @@ -355,6 +355,7 @@ * widget menu functions */ +/* static gboolean ui_button_press_event(GtkWidget *widget, GdkEvent *event, GtkMenu *menu) { if(event->type == GDK_BUTTON_PRESS) { GdkEventButton *e = (GdkEventButton*)event; @@ -389,6 +390,7 @@ gtk_menu_popup(menu, NULL, NULL, 0, 0, 0, gtk_get_current_event_time()); #endif } +*/ void ui_widget_menuitem(UiObject *obj, char *label, ui_callback f, void *userdata) { ui_widget_menuitem_gr(obj, label, f, userdata, -1);