6 Jul
2017
6 Jul
'17
10:46 p.m.
Good evening,
Neither changing nor removing the "video=" part of the /etc/default/grub file had any effect. But the bigness of the font in the real-time boot log display is a cosmetic issue. The grub menu is now as it should be, and the system boots correctly. That was the real issue. So I consider this issue solved.
I thank everyone who tried to help. This home user could not have done it without you.
Bill.