diff --git a/makedist.pl b/makedist.pl index f96ee77d3..2b2a6db20 100755 --- a/makedist.pl +++ b/makedist.pl @@ -147,6 +147,14 @@ if (!$release || !-d "$tardir/$dir") { if (!$min && -r "$tardir/$dir/gray-theme") { system("cd $tardir/$dir && ln -s gray-theme blue-theme"); } + + # ZIP up all help pages + print "Zipping up help pages\n"; + foreach $help (map { "$tardir/$dir/$_/help" } @mlist) { + if (-d $help) { + system("cd $help && zip help.zip *.html >/dev/null && rm -f *.html"); + } + } } # Store release version, if set