diff options
| author | Peter Eisentraut <peter_e@gmx.net> | 2018-02-23 19:52:30 -0500 |
|---|---|---|
| committer | Peter Eisentraut <peter_e@gmx.net> | 2018-02-28 09:26:36 -0500 |
| commit | 6d933da306c993ab52a28dba9f4f5b80c80f9681 (patch) | |
| tree | 4466d4da7794becdfa7fb58fac8999278c882d09 /src/backend/executor | |
| parent | d21ddc220fc735da84c9fa7bae1968f6953a6c8c (diff) | |
| download | postgresql-6d933da306c993ab52a28dba9f4f5b80c80f9681.tar.gz postgresql-6d933da306c993ab52a28dba9f4f5b80c80f9681.zip | |
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.
Diffstat (limited to 'src/backend/executor')
0 files changed, 0 insertions, 0 deletions