diff options
Diffstat (limited to 'resources/tools')
-rwxr-xr-x | resources/tools/doc_gen/run_doc.sh | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/resources/tools/doc_gen/run_doc.sh b/resources/tools/doc_gen/run_doc.sh index f4e41e5de4..ca955cc6c4 100755 --- a/resources/tools/doc_gen/run_doc.sh +++ b/resources/tools/doc_gen/run_doc.sh @@ -45,7 +45,8 @@ export PYTHONPATH=`pwd` find ./${WORKING_DIR}/env -type f -name '*.rst' | xargs rm -f # Generate the documentation: -sphinx-build -v -b html ${WORKING_DIR} ${BUILD_DIR}/ +DATE=$(date -u '+%d-%b-%Y') +sphinx-build -v -c ${WORKING_DIR} -a -b html -E -D release=$1 -D version="$1 documentation - $DATE" ${WORKING_DIR} ${BUILD_DIR}/ find . -type d -name 'env' | xargs rm -rf |