Hi Marcin, Marcin Borkowski <mb...@wmi.amu.edu.pl> writes:
> Just a n00b's (and IANAL's) 2cents here: what about including the GFDL > in, say 5pt font? Yes, it is awful, but at least does not take up > dozens of pages... Yes -- but I don't know how to set the font to 5pt in .texi files. AFAIK, you can change the font _globally_ to @fonttextsize 10 or 11, but not for one section only and not below 10pt... I'd be glad to be wrong of course ! -- Bastien
