+ stdio_devices[file]->putc(stdio_devices[file], c);
+}
+
+#ifdef CONFIG_PRE_CONSOLE_BUFFER
+static inline void console_puts_noserial(int file, const char *s)
+{
+ if (strcmp(stdio_devices[file]->name, "serial") != 0)
+ stdio_devices[file]->puts(stdio_devices[file], s);