# CONFIG_HIGHMEM4G is not set