# CONFIG_PPC_86xx is not set