Generate Linux man pages when generating docs.

1 files changed, 9 insertions, 0 deletions

diff --git a/dist/s_docs b/dist/s_docs
index 208ed95fc3e..55e4557e234 100755
--- a/dist/s_docs
+++ b/dist/s_docs
@@ -103,6 +103,15 @@ EOF
 	(cd ../docs &&
 	    sed -i~ -e 's,/\.html,/,' -e 's,\.html\.html,.html,' navtree.js &&
 	    rm -f navtree.js~)
+
+	# Fixup the man pages generated by Doxygen. We want the command line
+	# documentation to be the main man page, but also install a man page
+	# for the WiredTiger header into the library section.
+	(cd ../docs && mkdir -p man/man1 &&
+	    mv man/man3/command_line.3 man/man1/wt.1 &&
+	    sed -i~ -e 's/command_line/wt/g' man/man1/wt.1 &&
+	    mv man/man3/wt.3 man/ && rm -f man/man3/* &&
+	    mv man/wt.3 man/man3/wiredtiger.3)
 }
 
 clean=0