diff options
Diffstat (limited to 'resources/tools/doc_gen/run_doc.sh')
| -rwxr-xr-x | resources/tools/doc_gen/run_doc.sh | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/resources/tools/doc_gen/run_doc.sh b/resources/tools/doc_gen/run_doc.sh index 1a037071a5..544554e93c 100755 --- a/resources/tools/doc_gen/run_doc.sh +++ b/resources/tools/doc_gen/run_doc.sh @@ -41,8 +41,11 @@ export PYTHONPATH=`pwd` # Generate rst files: ./gen_rst.py +# Remove all rst files from ./${WORKING_DIR}/env directory - we do not need them +find ./${WORKING_DIR}/env -type f -name '*.rst' | xargs rm -f + # Generate the documentation: -sphinx-build -vvv -b html ${WORKING_DIR}/ ${BUILD_DIR}/ +sphinx-build -v -b html ${WORKING_DIR} ${BUILD_DIR}/ find . -type d -name 'env' | xargs rm -rf |