> I would like a general opinion about the filenames to use. Should we use > > /boot/gnumach.gz > /boot/serverboot.gz > > for the gzip'ed files, or should we store the gzip'ed files under the > standard names > > /boot/gnumach > /boot/serverboot
I'd lean toward the first, as it gives users a good visual cue about the content of the file. Having to change the filename in the menu.lst at this point of development shouldn't be that unreasonable of a demand :) We need to promote a consistent and reasonably intuitive system for the users, and I personally feel that the benefits of adding the .gz extension far outweigh the "hassles" of a one-time change in the menu config. Yours for free software, ed.
