Bug#718344: GRUB_DEFAULT vs. submenus

[jidanni at jidanni.org]

Package: grub2-common
Version: 2.00-15
File: /usr/share/info/grub.info.gz

On # (info "(grub) Simple configuration") there is mentioned

`GRUB_DEFAULT'
     The default menu entry.  This may be a number, in which case
     it...

The problem is that it does not mention how it works in the case of
submenus,

(info "(grub) submenu")

or Debian's submenus, which by the way there is no simple way to turn off.