diff --git a/docs_src/deploy_book.sh b/docs_src/deploy_book.sh index fc335bf0..4be190e7 100755 --- a/docs_src/deploy_book.sh +++ b/docs_src/deploy_book.sh @@ -116,7 +116,7 @@ if [[ $? -ne 0 ]]; then fi exit 1 fi -git push +git push --force if [[ $? -ne 0 ]]; then echo "- deploy_book: ERROR: ******** Error during push! ********" exit 1