# CONFIG_ARCH_IXP4XX is not set