Peter Eisentraut <peter.eisentr...@2ndquadrant.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