diff --git a/repos/base-sel4/doc/notes.txt b/repos/base-sel4/doc/notes.txt
index 6c968c1b0f..47294a23cd 100644
--- a/repos/base-sel4/doc/notes.txt
+++ b/repos/base-sel4/doc/notes.txt
@@ -762,20 +762,19 @@ The next problem is more tricky:
 ! include/sel4/arch/syscalls.h:481:6: error: impossible register constraint in ‘asm’
 
 The error refers to the system-call binding for 'seL4_DebugPutChar'. After
-twiddling with the asm constraints, it turns
-out that the error is caused by the use of an enum value as input argument.
-The C++ compiler is free to pick any integer type that it sees fit for
-representing an enum value. Even though the seL4 developers use a helper
-macro (SEL4_FORCE_LONG_ENUM) to force a certain minimum bit width for the
-used type, the C++ compiler complains. By explicitly casting the input
-argument to 'int', this ambiguity can be resolved and the compiler becomes
-happy. Unfortunately, this means that I will have to patch the system-call
-bindings to make them fit for the use with C++. But looking at the bindings,
-I think that a patch won't be avoidable anyway because the bindings clobber
-the EBX register. This means that we won't be able to use the headers for
-compiling position-independent code (as is the case for Genode). For now,
-we have are not compiling with '-fPIC' enabled but this issue is clear
-in front of us.
+twiddling with the asm constraints, it turns out that the error is caused by
+the use of an enum value as input argument. The C++ compiler is free to pick
+any integer type that it sees fit for representing an enum value. Even though
+the seL4 developers use a helper macro (SEL4_FORCE_LONG_ENUM) to force a
+certain minimum bit width for the used type, the C++ compiler complains. By
+explicitly casting the input argument to 'int', this ambiguity can be resolved
+and the compiler becomes happy. Unfortunately, this means that I will have to
+patch the system-call bindings to make them fit for the use with C++. But
+looking at the bindings, I think that a patch won't be avoidable anyway
+because the bindings clobber the EBX register. This means that we won't be
+able to use the headers for compiling position-independent code (as is the
+case for Genode). For now, we have are not compiling with '-fPIC' enabled but
+this issue is clear in front of us.
 
 Patches for the seL4 code will be reside at _base-sel4/src/kernel/_. E.g.,
 we just added the current modification of the _syscalls.h_ header by
@@ -802,10 +801,20 @@ built. Executing the run script produces the result that we longed for:
 The first line is produced by our test program. Knowing how to print
 characters using the kernel's debug interface, filling out the empty
 stub function 'Genode::Core_console::_out_char' in _core_console.h_
-is easy.
-
-
-
-
+is easy. We can replace the main program with this version:
+
+! #include <base/printf.h>
+! 
+! int main()
+! {
+! 	PDBG("a message printed via Genode's PDBG");
+! 
+! 	*(int *)0x1122 = 0;
+! 	return 0;
+! }
+
+When running it via 'make run/test', it produces the expected result:
+
+! int main(): a message printed via Genode's PDBG
 
 
diff --git a/repos/base-sel4/src/base/console/core_console.h b/repos/base-sel4/src/base/console/core_console.h
index 738acda036..c3db89a2d6 100644
--- a/repos/base-sel4/src/base/console/core_console.h
+++ b/repos/base-sel4/src/base/console/core_console.h
@@ -11,8 +11,12 @@
  * under the terms of the GNU General Public License version 2.
  */
 
+/* Genode includes */
 #include <base/console.h>
 
+/* seL4 includes */
+#include <sel4/arch/functions.h>
+#include <sel4/arch/syscalls.h>
 
 namespace Genode
 {
@@ -20,8 +24,10 @@ namespace Genode
 	{
 		protected:
 
-			void _out_char(char c) { }
+			void _out_char(char c)
+			{
+				seL4_DebugPutChar(c);
+			}
 	};
 }
 
-
diff --git a/repos/base-sel4/src/test/sel4/main.cc b/repos/base-sel4/src/test/sel4/main.cc
index 79da67730a..4ced82d184 100644
--- a/repos/base-sel4/src/test/sel4/main.cc
+++ b/repos/base-sel4/src/test/sel4/main.cc
@@ -12,17 +12,11 @@
  */
 
 /* Genode includes */
-#include <util/string.h>
-
-/* seL4 includes */
-#include <sel4/arch/functions.h>
-#include <sel4/arch/syscalls.h>
+#include <base/printf.h>
 
 int main()
 {
-	char const *string = "\nMessage printed via the kernel\n";
-	for (unsigned i = 0; i < Genode::strlen(string); i++)
-		seL4_DebugPutChar(string[i]);
+	PDBG("a message printed via Genode's PDBG");
 
 	*(int *)0x1122 = 0;
 	return 0;
diff --git a/repos/base-sel4/src/test/sel4/thread.cc b/repos/base-sel4/src/test/sel4/thread.cc
index 1a8f7cb4bf..83670d86ba 100644
--- a/repos/base-sel4/src/test/sel4/thread.cc
+++ b/repos/base-sel4/src/test/sel4/thread.cc
@@ -46,8 +46,6 @@ Thread_base::Thread_base(size_t, const char *name, size_t stack_size, Type type,
 {
 	strncpy(_context->name, name, sizeof(_context->name));
 	_context->thread_base = this;
-
-	_init_platform_thread(type);
 }
 
 
@@ -55,4 +53,4 @@ Thread_base::Thread_base(size_t quota, const char *name, size_t stack_size, Type
 : Thread_base(quota, name, stack_size, type, nullptr) { }
 
 
-Thread_base::~Thread_base() { _deinit_platform_thread(); }
+Thread_base::~Thread_base() { }