# CONFIG_PPC_BOOK3E_64 is not set