# CONFIG_PPC_LITE5200 is not set
