--- src/gui/debugger/dbg_dock.c.orig 2010-11-07 00:02:53.000000000 +0100 +++ src/gui/debugger/dbg_dock.c 2010-11-07 00:03:21.000000000 +0100 @@ -151,22 +151,22 @@ void dbgdock_show_all(int all) { - if(!GTK_WIDGET_VISIBLE(dbgw.dock) && all) + if(!gtk_widget_get_visible(dbgw.dock) && all) gtk_widget_show(dbgw.dock); - if(GTK_WIDGET_VISIBLE(dbgw.iop)) + if(gtk_widget_get_visible(dbgw.iop)) gtk_window_iconify(GTK_WINDOW(dbgw.iop)); - if(GTK_WIDGET_VISIBLE(dbgw.pclog)) + if(gtk_widget_get_visible(dbgw.pclog)) gtk_window_iconify(GTK_WINDOW(dbgw.pclog)); } void dbgdock_hide_all(int all) { - if(GTK_WIDGET_VISIBLE(dbgw.dock) && all) + if(gtk_widget_get_visible(dbgw.dock) && all) gtk_widget_hide(dbgw.dock); - if(GTK_WIDGET_VISIBLE(dbgw.pclog)) + if(gtk_widget_get_visible(dbgw.pclog)) gtk_widget_hide(dbgw.pclog); - if(GTK_WIDGET_VISIBLE(dbgw.iop)) + if(gtk_widget_get_visible(dbgw.iop)) gtk_widget_hide(dbgw.iop); } \ No newline at end of file