# CONFIG_MPENTIUMII is not set