diff --git a/src/kernel/core/debug.c b/src/kernel/core/debug.c
index b41fa7bcbb..bcb7ecb478 100644
--- a/src/kernel/core/debug.c
+++ b/src/kernel/core/debug.c
@@ -14,6 +14,7 @@
 #include <gdb.h>
 #include <Errors.h>
 #include <int.h>
+#include <vm.h>
 
 #include <arch/dbg_console.h>
 #include <arch/debug.h>
diff --git a/src/kernel/core/syscalls.c b/src/kernel/core/syscalls.c
index ca79426496..3c20901a8c 100644
--- a/src/kernel/core/syscalls.c
+++ b/src/kernel/core/syscalls.c
@@ -423,6 +423,10 @@ syscall_dispatcher(unsigned long call_num, void *arg_buffer, uint64 *call_ret)
 		case SYSCALL_GETENV:
 			*call_ret = user_getenv((const char *)arg0, (char **)arg1);
 			break;
+		case SYSCALL_DEBUG_OUTPUT:
+			_user_debug_output((const char *)arg0);
+			break;
+
 		case SYSCALL_GET_THREAD_INFO:
 			*call_ret = user_get_thread_info((thread_id)arg0, (thread_info *)arg1);
 			break;