# CONFIG_PPC_4K_PAGES is not set