Bug#726264: grub-set-default seems not to be documented on (info "(grub) Simple configuration")

[jidanni at jidanni.org]

Package: grub2-common
Version: 2.00-19
Severity: wishlist
File: /usr/sbin/grub-set-default

(info "(grub) Simple configuration") should mention grub-set-default as
a quicker way...

P.S., The info page mentioned on the grub-set-default man page is missing.