[coreboot] Re: 'make menuconfig' broken by commit 7eab8ef8b720e8744eea3c6c771bccc217fbe5ed