# CONFIG_PPC_MICROWATT is not set
