build: Compress man pages.
authorAndre Noll <maan@tuebingen.mpg.de>
Sun, 3 Mar 2019 20:58:45 +0000 (21:58 +0100)
committerAndre Noll <maan@tuebingen.mpg.de>
Thu, 14 Mar 2019 13:11:03 +0000 (14:11 +0100)
commitf35b70fc3e8656f71437cc85062da31488acd781
tree7294651f928370d1327b9da09fc6b81fa910c87b
parente28bd04447619b06af565adc247c9ddeecc2d286
build: Compress man pages.

Man pages should always be installed in compressed form, so run gzip
on all four man pages. We always specify -f so that gzip won't ask
questions, and use the highest compression level because the pages
are compressed only once and decompressed every time the man page
is opened.
.gitignore
Makefile