Peter Eisentraut <peter(dot)eisentraut(at)2ndquadrant(dot)com> writes:
> On 2020-04-29 21:58, Tom Lane wrote:
>> I think making the built documentation depend on nonstandard fonts
>> is a truly awful idea. It'd be okay perhaps if the requirement only
>> applied to people building the docs, but won't the requirement also
>> flow through to end users?
> No, the font is embedded into the built PDF.
Ah. Well, if it doesn't enlarge the file very much, I guess that'd
be fine.
regards, tom lane