# CONFIG_SERIAL_KGDB_NMI is not set