diff options
Diffstat (limited to 'doc/do_docs')
| -rwxr-xr-x | doc/do_docs | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/doc/do_docs b/doc/do_docs index 531081eba9..0f0a08a514 100755 --- a/doc/do_docs +++ b/doc/do_docs @@ -15,7 +15,14 @@ extra_manuals="hwapi" # posix_users manual left out until finished # ada_user manual left out until bindings released +if [ x${MANUAL_SET} = x ] ; then + MANUAL_SET=public +fi + case ${MANUAL_SET} in + public) + manuals="$public_docs" + ;; support) manuals="$public_docs $support_docs" ;; @@ -26,7 +33,7 @@ case ${MANUAL_SET} in manuals="$public_docs $support_docs $partners_docs $extra_manuals" ;; *) - echo "ERROR: Unknown manual set $(MANUAL_SET)" + echo "ERROR: Unknown manual set ${MANUAL_SET}" exit 1 ;; esac |