# CONFIG_PPC_PS3 is not set