From 044fa385fc23f9553b4f23cb9547c7d2fe88f408 Mon Sep 17 00:00:00 2001
From: Pascal Thomet <pthomet@gmail.com>
Date: Tue, 6 Feb 2024 09:24:46 +0100
Subject: [PATCH] deploy_book: git push force

---
 docs_src/deploy_book.sh | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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