deploy_book: git push force

pthom · Feb 6, 2024 · 044fa38 · 044fa38
1 parent c843d5c
commit 044fa38
Showing 1 changed file with 1 addition and 1 deletion.
diff --git 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