# CONFIG_TTY_PRINTK is not set