# CONFIG_ARCH_LPC32XX is not set