fix: merge strategy choice

.github/workflows/mirror_docs_repo.yml

@@ -20,6 +20,19 @@ jobs:
 
       - name: Push to branch
         run: |
+	  HISTORY_BRANCH=aztec-bot/docs-git-subrepo-history
+          if git rev-parse --verify --quiet $HISTORY_BRANCH ; then
+	    # we already have this history, merge it
+            git checkout $HISTORY_BRANCH
+	    # we avoid anything except git subrepo file updates in th history branch
+            git merge -X theirs --no-commit ad/fix/mirror-runner 
+          else
+	    # create a new branch based on ours
+            git checkout -b $HISTORY_BRANCH
+          fi
           git config --global user.email "[email protected]"
           git config --global user.name "AztecBot"
+          # push to docs repo, commit locally
           ./scripts/git_subrepo.sh push docs --branch=main
+	  # push new commit to the history branch, overwrite during conflicts
+	  git push origin $HISTORY_BRANCH --force