casa-mp-base

--- 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)