# CONFIG_THUMB2_KERNEL is not set