Re: downsized grub menu. [CLOSED]

[Tim]

Patrick O'Callaghan:
> IIRC it used to be 72.72 (my first job was working on an early
> typesetting system at Cambridge University Press :-) However
> according to Wikipedia a point is now officially 1/72 of an
> "international inch":
>
> https://en.wikipedia.org/wiki/Point_(typography)

I stayed with "approx" since it never was specific (different companies
had differing point sizes), and I wouldn't be surprised if different
companies (e.g. printing houses), still have their own ideas about the
thing.  ;-)

And then you have the issue of different inches, too.

And if you printed out the built-in test pages of different printers,
I'm sure you'll find that 12 point Times on one printer is not
identical to 12 point Times on another.  It certainly was when I've
done that in the past.