doc: Improve man build speed

Peter Eisentraut <peter_e@gmx.net>

Commit: 6d933da306c993ab52a28dba9f4f5b80c80f9681
Author: Peter Eisentraut <peter_e@gmx.net>
Date: 2018-02-28T14:26:36Z
Releases: 11.0
doc: Improve man build speed

Turn off man.endnotes.are.numbered parameter, which we don't need, but
which increases performance vastly if off.  Also turn on
man.output.quietly, which also makes things a bit faster, but which is
also less useful now as a progress indicator because the build is so
fast now.

Files

PathChange+/−
doc/src/sgml/stylesheet-man.xsl modified +3 −1