XXX1: distrib/notes/common/contents needs to be updated as noted in comment XXX2: should we also build VIRTEX kernels?