sajolida authored Mar 20, 2020 and intrigeri committed Mar 21, 2020

People might be faced with either GRUB or SYSLINUX and have to perform
different procedures to edit the boot options.

GRUB is already named on the screen.

Naming SYSLINUX will make it easier to write the doc and for people to
relate to which of the 2 boot loaders they get.