# CONFIG_IWMMXT is not set