# CONFIG_NOHIGHMEM is not set