Re: naming of gzip'ed gnumach and serverboot

["Ed Boraas" <ed@concordia.ab.ca>]

> 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.