Which is best:
1. completely remove the "video=vesa:off" from the GRUB_CMDLINE_LINUX line,
2. change the "off" to "on" in that line?
I would not be surprised if it could make it significant difference.
The font used in the grub menu and the grub shell has been a good size all along, and has
not changed. The only changes I made to the grub file are those that you advised.
Everything else in that file, including that "video=vesa:off", is either
"factory settings", or put there last month by "Boot-Repair-Disk", or
put there by the quasi-weekly "dnf upgrade" run, or put there by the
quasi-semi-annual upgrade from f[n] to f[n+1].