Please drop the debian/default/grub change. It'll probably cause configuration file prompts for people, and it's unnecessary - most variables are not documented by way of comments in the stock /etc/default/grub file.
Conversely, please add a patch to docs/grub.texi to document this new variable.
Please drop the debian/default/grub change. It'll probably cause configuration file prompts for people, and it's unnecessary - most variables are not documented by way of comments in the stock /etc/default/grub file.
Conversely, please add a patch to docs/grub.texi to document this new variable.