(mike@: actually no sense to set both
KFLAVOURS and STAGE1_KFLAVOUR to the same value
since the latter is derived from the former)