# CONFIG_MPENTIUM4 is not set