Index: generic/src/debug/print.c
===================================================================
--- generic/src/debug/print.c	(revision 91ef0d955c68876ca16fffef6f8e7416dfdefff5)
+++ generic/src/debug/print.c	(revision dc747e33f6f5d74c7d1b7b50fda3b2fabff8fa82)
@@ -36,6 +36,6 @@
 #include <arch.h>
 
-static char digits[] = "0123456789abcdef"; /**< Hexadecimal characters */
-static spinlock_t printflock;              /**< printf spinlock */
+static char digits[] = "0123456789abcdef"; 	/**< Hexadecimal characters */
+SPINLOCK_INITIALIZE(printflock);		/**< printf spinlock */
 
 #define DEFAULT_DOUBLE_PRECISION 16