Index: kernel/generic/src/syscall/syscall.c
===================================================================
--- kernel/generic/src/syscall/syscall.c	(revision 15b376117118b2997d1424676143cb9b7008707b)
+++ kernel/generic/src/syscall/syscall.c	(revision e515a82717878d1a0549c75f5eebb3a907f2f15d)
@@ -55,11 +55,4 @@
 #include <console/console.h>
 #include <udebug/udebug.h>
-
-/** Print a hex integer into klog */
-static sysarg_t sys_debug_putint(sysarg_t i)
-{
-	printf("[task:0x%x]", (unsigned) i);
-	return 0;
-}
 
 /** Dispatch system call */
@@ -187,5 +180,4 @@
 	
 	/* Debug calls */
-	(syshandler_t) sys_debug_putint,
 	(syshandler_t) sys_debug_enable_console,
 	(syshandler_t) sys_debug_disable_console