H. Peter Anvin 3d61238bf8 ps/pdf doc: default to 10-point font, wider leading
Switch the main font to 10 points Times Roman, but leave the leading
at 11 points.  This produces, in my opinion, a much more legible and
printable document.
2008-06-11 18:09:02 -07:00
..
2007-09-12 21:05:06 -07:00
2008-06-11 18:07:40 -07:00