Sounds good, thanks. Note that if you're using GRUB_TIMEOUT_STYLE, then GRUB_HIDDEN_TIMEOUT is supposed to be ignored; once GRUB_TIMEOUT_STYLE is set to indicate that we're in the new world, we use GRUB_TIMEOUT consistently.
Sounds good, thanks. Note that if you're using GRUB_TIMEOUT_STYLE, then
GRUB_HIDDEN_TIMEOUT is supposed to be ignored; once GRUB_TIMEOUT_STYLE
is set to indicate that we're in the new world, we use GRUB_TIMEOUT
consistently.