Peter Eisentraut <[email protected]> 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
