diff options
Diffstat (limited to 'doc/do_docs')
-rwxr-xr-x | doc/do_docs | 9 |
1 files changed, 3 insertions, 6 deletions
diff --git a/doc/do_docs b/doc/do_docs index 792c5b643a..46949dc81b 100755 --- a/doc/do_docs +++ b/doc/do_docs @@ -23,14 +23,11 @@ fi case ${MANUAL_SET} in public) - manuals="$public_docs" - ;; - support) + # manuals="$public_docs" + # ;; + #support) manuals="$public_docs $support_docs" ;; - partners) - manuals="$public_docs $support_docs $partners_docs" - ;; *) echo "ERROR: Unknown manual set ${MANUAL_SET}" exit 1 |