[Date Prev][Date Next] [Thread Prev][Thread Next] [Date Index] [Thread Index]

Re: naming of gzip'ed gnumach and serverboot

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

Reply to: