diff --git a/libsel4platsupport/src/common.c b/libsel4platsupport/src/common.c index a1f130e5..a8fa0238 100644 --- a/libsel4platsupport/src/common.c +++ b/libsel4platsupport/src/common.c @@ -268,8 +268,8 @@ static void __serial_setup() case NOT_INITIALIZED: #ifdef CONFIG_LIB_SEL4_PLAT_SUPPORT_USE_SEL4_DEBUG_PUTCHAR setup_status = SETUP_COMPLETE; - printf("\nWarning: using printf before serial is set up. This only works as your\n"); - printf("printf is backed by seL4_Debug_PutChar()\n"); + seL4_DebugPutString("\nWarning: using printf before serial is set up. This only works as your\n" + "printf is backed by seL4_Debug_PutChar()\n"); started_regular = 1; #else /* attempt failsafe initialization and print something out */