diff options
-rwxr-xr-x | maketgz | 6 |
1 files changed, 6 insertions, 0 deletions
@@ -78,6 +78,12 @@ fi ############################################################################ # +# Make sure we have updated HTML versions of all man pages: +# +make html + +############################################################################ +# # Now run make dist # |