Index: kernel/generic/src/main/version.c
===================================================================
--- kernel/generic/src/main/version.c	(revision 9efff92fe17a9135c9577f15b3c4d7bb711366c2)
+++ kernel/generic/src/main/version.c	(revision 6c39a9074d1bf9a23bf5243a2c35b2a8549f41d3)
@@ -59,5 +59,5 @@
 {
 	printf("%s, release %s (%s)%s\nBuilt%s for %s\n%s\n",
-		project, release, name, revision, timestamp, arch, copyright);
+	    project, release, name, revision, timestamp, arch, copyright);
 }
 
Index: kernel/generic/src/printf/printf.c
===================================================================
--- kernel/generic/src/printf/printf.c	(revision 9efff92fe17a9135c9577f15b3c4d7bb711366c2)
+++ kernel/generic/src/printf/printf.c	(revision 6c39a9074d1bf9a23bf5243a2c35b2a8549f41d3)
@@ -34,4 +34,5 @@
 
 #include <print.h>
+#include <stdarg.h>
 
 int printf(const char *fmt, ...)
Index: kernel/generic/src/printf/printf_core.c
===================================================================
--- kernel/generic/src/printf/printf_core.c	(revision 9efff92fe17a9135c9577f15b3c4d7bb711366c2)
+++ kernel/generic/src/printf/printf_core.c	(revision 6c39a9074d1bf9a23bf5243a2c35b2a8549f41d3)
@@ -46,16 +46,23 @@
 /** show prefixes 0x or 0 */
 #define __PRINTF_FLAG_PREFIX       0x00000001
+
 /** signed / unsigned number */
 #define __PRINTF_FLAG_SIGNED       0x00000002
+
 /** print leading zeroes */
 #define __PRINTF_FLAG_ZEROPADDED   0x00000004
+
 /** align to left */
 #define __PRINTF_FLAG_LEFTALIGNED  0x00000010
+
 /** always show + sign */
 #define __PRINTF_FLAG_SHOWPLUS     0x00000020
+
 /** print space instead of plus */
 #define __PRINTF_FLAG_SPACESIGN    0x00000040
+
 /** show big characters */
 #define __PRINTF_FLAG_BIGCHARS     0x00000080
+
 /** number has - sign */
 #define __PRINTF_FLAG_NEGATIVE     0x00000100
@@ -79,8 +86,8 @@
 } qualifier_t;
 
-static char nullstr[] = "(NULL)";
-static char digits_small[] = "0123456789abcdef";
-static char digits_big[] = "0123456789ABCDEF";
-static char invalch = U_SPECIAL;
+static const char *nullstr = "(NULL)";
+static const char *digits_small = "0123456789abcdef";
+static const char *digits_big = "0123456789ABCDEF";
+static const char invalch = U_SPECIAL;
 
 /** Print one or more characters without adding newline.
@@ -351,5 +358,5 @@
     uint32_t flags, printf_spec_t *ps)
 {
-	char *digits;
+	const char *digits;
 	if (flags & __PRINTF_FLAG_BIGCHARS)
 		digits = digits_big;
