# CONFIG_MPENTIUMM is not set