José Matos wrote: > Another file format increment. :-) Sorry about that.
> If you want I will have a look into it.
Yes, please.
> Correct me if I am wrong, we can
> abuse the Options field to add the missing fontsize, right?
Yes. For \paperfontsize {10,11,12}, just put 10pt, 11pt or 12pt to the options
field and set the fontsize to default.
Thanks,
Jürgen
