fix: push core docs release to gh-pages once

Run mike deploy and set-default locally, then push
gh-pages once so GitHub Pages builds a single time
per release tag.

Signed-off-by: Frederic Pillon <frederic.pillon@st.com>
Assisted-by: GitHub Copilot: Claude Haiku 5.5

Author: fpistm

.github/workflows/publish-docs.yml

@@ -73,9 +73,14 @@ jobs:
             exit 1
           fi
           latest=$(git tag --list | grep -E '^[0-9]+\.[0-9]+\.[0-9]+$' | sort -V | tail -n 1)
+          if git ls-remote --exit-code --heads pages gh-pages >/dev/null; then
+            git fetch pages gh-pages:gh-pages
+          fi
           if [[ "$VERSION" == "$latest" ]]; then
-            mike deploy --remote pages --branch gh-pages --update-aliases --push "$VERSION" latest
-            mike set-default --remote pages --branch gh-pages --push latest
+            mike deploy --branch gh-pages --update-aliases "$VERSION" latest
+            mike set-default --branch gh-pages latest
           else
-            mike deploy --remote pages --branch gh-pages --push "$VERSION"
+            mike deploy --branch gh-pages "$VERSION"
           fi
+          # One push so GitHub Pages builds the site once.
+          git push pages gh-pages