From 3df7953d7a04ac64b5439fb35dc9ce3be97600c8 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Julien=20D=C3=A9ramond?= <juderamond@gmail.com>
Date: Thu, 12 Jun 2025 06:54:12 +0200
Subject: [PATCH] Delete local branch if already existing

---
 build/docs-prep.sh | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/build/docs-prep.sh b/build/docs-prep.sh
index 812222d55f..357768abea 100755
--- a/build/docs-prep.sh
+++ b/build/docs-prep.sh
@@ -92,6 +92,12 @@ fi
 print_success "Pulled latest changes from origin/gh-pages"
 
 # Step 4: Create a new branch for the update
+print_info "Checking if branch ${NEW_BRANCH} exists and deleting it if it does…"
+if git show-ref --verify --quiet refs/heads/${NEW_BRANCH}; then
+  execute "git branch -D ${NEW_BRANCH}"
+else
+  print_info "Branch ${NEW_BRANCH} does not exist, proceeding with creation…"
+fi
 print_info "Creating new branch ${NEW_BRANCH}…"
 execute "git checkout -b ${NEW_BRANCH}"