Update gh-pages before mike run, cont'd

Signed-off-by: Roberto Di Cosmo <[email protected]>
swhid · Aug 9, 2023 · a79a1e0 · a79a1e0
1 parent 725d8ef
commit a79a1e0
Showing 1 changed file with 2 additions and 3 deletions.
diff --git a/.github/workflows/publish-dev.yml b/.github/workflows/publish-dev.yml
@@ -8,7 +8,7 @@ jobs:
     runs-on: ubuntu-latest
     container: python:3
     steps:
-    - uses: actions/checkout@v2
+    - uses: actions/checkout@v3
       with:
         ref: 'main'
     - name: Install pre-requisites
@@ -19,11 +19,10 @@ jobs:
       run: mkdocs build -v --clean
     - name: Configure Git user
       run: |
+         git fetch origin gh-pages --depth=1
          git config --global user.email "github-actions[bot]@users.noreply.github.com"
          git config --global user.name "github-actions[bot]"
          git config --global --add safe.directory '*'
     - name: Deploy MkDoc with mike 🚀
       run: |
-         git fetch origin gh-pages
-         git merge origin/gh-pages
          mike deploy --push dev