# CONFIG_PPC_83xx is not set