--- src/gui/debugger/dbg_code.c.orig	2010-08-19 12:25:41.000000000 +0200
+++ src/gui/debugger/dbg_code.c	2010-08-19 12:33:04.000000000 +0200
@@ -1096,7 +1096,7 @@
 
 int dbgcode_quit_enabled(void)
 {
-	return GTK_WIDGET_SENSITIVE(mi.m8);
+	return gtk_widget_get_sensitive(mi.m8);
 }
 
 static int close_debugger_wrapper(gpointer data)