projects / users / andresfreund / postgres.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: d21ddc2) | patch
doc: Improve man build speed
authorPeter Eisentraut <peter_e@gmx.net>
Sat, 24 Feb 2018 00:52:30 +0000 (19:52 -0500)
committerPeter Eisentraut <peter_e@gmx.net>
Wed, 28 Feb 2018 14:26:36 +0000 (09:26 -0500)
commit6d933da306c993ab52a28dba9f4f5b80c80f9681
tree4466d4da7794becdfa7fb58fac8999278c882d09tree
parentd21ddc220fc735da84c9fa7bae1968f6953a6c8ccommit | diff
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.
doc/src/sgml/stylesheet-man.xsl diff | blob | blame | history
Andres' PG stuff