diff --git a/apps/fibonacci/fibonacci.c b/apps/fibonacci/fibonacci.c
index 063cc4a..8182279 100644
--- a/apps/fibonacci/fibonacci.c
+++ b/apps/fibonacci/fibonacci.c
@@ -10,11 +10,11 @@
  * SPDX-License-Identifier: Apache-2.0
  */
 
+#include <kernel/gen_config.h>
+#include <sel4/arch/syscalls.h>
+#include <stdarg.h>
 #include <stdint.h>
 #include <stdio.h>
-#include <stdarg.h>
-
-#include <sel4/arch/syscalls.h>
 
 __thread seL4_IPCBuffer *__sel4_ipc_buffer;
 
@@ -45,6 +45,7 @@ __attribute__((naked)) void _start() {
 
 // only prints 32-bit "%x" hex values
 void minisel_printf(const char *fmt, ...) {
+#if CONFIG_PRINTING
   va_list args;
   va_start(args, fmt);
   for (; *fmt; fmt++) {
@@ -74,6 +75,7 @@ void minisel_printf(const char *fmt, ...) {
     }
   }
   va_end(args);
+#endif
 }
 
 typedef uint64_t interrupt_count_t;
diff --git a/apps/hello/hello.c b/apps/hello/hello.c
index eabd45f..1749991 100644
--- a/apps/hello/hello.c
+++ b/apps/hello/hello.c
@@ -9,10 +9,10 @@
 // using the seL4_DebugPutChar syscall and is intended as a starting
 // point for low-level tests.
 
-#include <stdint.h>
-#include <stdarg.h>
-
+#include <kernel/gen_config.h>
 #include <sel4/arch/syscalls.h>
+#include <stdarg.h>
+#include <stdint.h>
 
 __thread seL4_IPCBuffer *__sel4_ipc_buffer;
 
@@ -36,6 +36,7 @@ __attribute__((naked)) void _start() {
 
 // only prints 32-bit "%x" hex values
 void minisel_printf(const char *fmt, ...) {
+#if CONFIG_PRINTING
   va_list args;
   va_start(args, fmt);
   for (; *fmt; fmt++) {
@@ -53,6 +54,7 @@ void minisel_printf(const char *fmt, ...) {
     }
   }
   va_end(args);
+#endif
 }
 
 int main(int a0, int a1, int a2, int a3) {