> I would like a general opinion about the filenames to use. Should we use > > /boot/gnumach.gz > /boot/serverboot.gz I think so. Nothing in the system cares what these file names are (as long as you tell GRUB the file name you are using), so their names should be what people would like to see.