ok, I've committed this change to the grub repository - it's trivial either way, so not worth the trouble of arguing. ;)
ok, I've committed this change to the grub repository - it's trivial either way, so not worth the trouble of arguing. ;)