# CONFIG_ARCH_MEDIATEK is not set