--- uae/src/tui.c	2018/04/24 17:00:15	1.1.1.9
+++ uae/src/tui.c	2018/04/24 17:05:45	1.1.1.11
@@ -15,7 +15,7 @@
 
 #include "config.h"
 #include "options.h"
-#include "threaddep/penguin.h"
+#include "threaddep/thread.h"
 #include "uae.h"
 #include "gensound.h"
 #include "joystick.h"
@@ -53,7 +53,7 @@ static void save_settings (void)
     tui_backup_optionsfile ();
     f = fopen (optionsfile, "w");
     if (f == NULL) {
-	fprintf (stderr, "Error saving options file!\n");
+	write_log ("Error saving options file!\n");
 	return;
     }
     save_options (f, &currprefs);
@@ -720,3 +720,11 @@ int gui_update (void)
 {
     return 0;
 }
+
+void gui_lock (void)
+{
+}
+
+void gui_unlock (void)
+{
+}