work around bug in menuconfig without DEVELOPER=1 (target arch)