# CONFIG_HIGHPTE is not set