diff --git a/src/kernel/core/debug/debug.c b/src/kernel/core/debug/debug.c
index 8430dbb231..9ddcd0a4d6 100644
--- a/src/kernel/core/debug/debug.c
+++ b/src/kernel/core/debug/debug.c
@@ -313,7 +313,7 @@ dbg_puts(const char *s)
 static int
 cmd_reboot(int argc, char **argv)
 {
-	shutdown(true);
+	arch_cpu_shutdown(true);
 	return 0;
 		// I'll be really suprised if this line ever runs! ;-)
 }