<html><head><meta name="color-scheme" content="light dark"></head><body><pre style="word-wrap: break-word; white-space: pre-wrap;">--- src/gui/debugger/dbg_regs.c.orig	2010-08-19 12:25:41.000000000 +0200
+++ src/gui/debugger/dbg_regs.c	2010-08-19 12:31:13.000000000 +0200
@@ -302,7 +302,7 @@
 		gtk_window_iconify(GTK_WINDOW(dbgw.regs));
 #endif
 
-	if(!GTK_WIDGET_VISIBLE(dbgw.regs) &amp;&amp; !options3.regs.closed)
+	if(!gtk_widget_get_visible(dbgw.regs) &amp;&amp; !options3.regs.closed)
 		gtk_widget_show(dbgw.regs);
 
 	return dbgw.regs;
</pre></body></html>