Skip to content

Commit 0dfa8c4

Browse files
committed
fix(ci): fetch gh-pages before publishing docs
mike deploy --push was rejected as a non-fast-forward because the runner never fetched the existing gh-pages branch from the pages remote. mike only syncs from an existing pages/gh-pages tracking ref and otherwise starts a new branch, which cannot be pushed over the published history. Fetch gh-pages from the pages remote when it exists, before the development and release publish steps. Assisted-by: GitHub Copilot:claude-sonnet-5.5 Signed-off-by: Frederic Pillon <frederic.pillon@st.com>
1 parent bb42ca0 commit 0dfa8c4

1 file changed

Lines changed: 5 additions & 0 deletions

File tree

‎.github/workflows/publish-docs.yml‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -49,6 +49,11 @@ jobs:
4949
env:
5050
PAGES_TOKEN: ${{ steps.pages-token.outputs.token }}
5151
run: git remote add pages "https://x-access-token:${PAGES_TOKEN}@github.com/stm32duino/stm32duino.github.io.git"
52+
- name: Fetch published documentation
53+
run: |
54+
if git ls-remote --exit-code --heads pages gh-pages >/dev/null; then
55+
git fetch pages gh-pages
56+
fi
5257
- name: Publish development documentation
5358
if: github.ref == 'refs/heads/main'
5459
run: |

0 commit comments

Comments
 (0)