From a79a1e0b80dea59632ec9cff10a7e3299e3bb128 Mon Sep 17 00:00:00 2001 From: Roberto Di Cosmo Date: Wed, 9 Aug 2023 12:13:41 +0200 Subject: [PATCH] Update gh-pages before mike run, cont'd Signed-off-by: Roberto Di Cosmo --- .github/workflows/publish-dev.yml | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/.github/workflows/publish-dev.yml b/.github/workflows/publish-dev.yml index 864673c..85605f1 100644 --- 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