diff -r 80edb1a93f7a -r 473c03f85197 ui/gtk/menu.c
--- 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);