(on Dec. 20, I said)
If, after a few days, the grub menu still looks good, I'll
promote this thread from CLOSED to SOLVED.
After a weekly patching, a few cycles of nightly power-down and morning
power-up, and a few days of regular operational use, I'm confident this
really is fixed. I'm upgrading this to SOLVED.
I thank participants for their help, and for the interesting discussion
on font sizes.