From e3fc5a79c3ec44e0b72db8ab107a611de1a6db73 Mon Sep 17 00:00:00 2001 From: Peter Eisentraut Date: Fri, 23 Feb 2018 19:52:30 -0500 Subject: [PATCH] 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 | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/doc/src/sgml/stylesheet-man.xsl b/doc/src/sgml/stylesheet-man.xsl index e9c407230c..691196525a 100644 --- a/doc/src/sgml/stylesheet-man.xsl +++ b/doc/src/sgml/stylesheet-man.xsl @@ -12,11 +12,13 @@ 0 0 +0 - + 32 40 +