[PATCH 0/1] docs: Fix numerous minor mistakes in grub.info

[Hans Ulrich Niedermann]

This patch does not change the intended meaning of the text
and only touches about the first 1300 of about 7000 lines
in docs/grub.texi. If there is interest in picking up this
patch, I intend to read through the rest of grub.texi as
well to find more of these easy fixes while adding remarks
for bigger issues which require actual text changes.

Then, I can start (with some help) addressing the issues
pointed to by these remarks like undocumented commands,
renamed commands, wrong and outdated instructions, remarks
about a future which has become present a long time ago, etc.

Uli