[coreboot] Question on switching memory stick from dimm_mask 0x01 to dimm_mask 0x10