diff options
-rwxr-xr-x | docs/makedocs.pl | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/docs/makedocs.pl b/docs/makedocs.pl index a5511d2c4..e46f7e7da 100755 --- a/docs/makedocs.pl +++ b/docs/makedocs.pl @@ -170,7 +170,9 @@ foreach my $lang (@langs) { make_pod() if $pod_simple; + next if grep { $_ eq '--pod-only' } @ARGV; + MakeDocs('HTML', 'make html'); MakeDocs('TXT', 'make text'); - MakeDocs('PDF', 'make latexpdf'); + MakeDocs('PDF', 'make latexpdf') if grep { $_ eq '--with-pdf' } @ARGV; } |