diff --git a/doc/build-doc.py b/doc/build-doc.py index 9a3846bb..517c6f28 100644 --- a/doc/build-doc.py +++ b/doc/build-doc.py @@ -368,6 +368,8 @@ def print_usage(appname, output): build_man = True if o == '--pdf': build_pdf = True + if o == '--all': + allowContrib = True if not args: print("error: build directory not specified\n", file=sys.stderr)