diff --git a/.github/workflows/publish_doc.yml b/.github/workflows/publish_doc.yml index bd37883d..2152a96a 100644 --- a/.github/workflows/publish_doc.yml +++ b/.github/workflows/publish_doc.yml @@ -4,6 +4,9 @@ on: push: branches: - main + pull_request: + paths: + - 'docs/**' workflow_dispatch: permissions: @@ -24,7 +27,19 @@ jobs: run: | git config user.name ${{ github.actor }} git config user.email ${{ github.actor }}@users.noreply.github.com - - run: | + - name: Delete existing doc + run: | + git fetch origin gh-pages + mike delete ${{ github.head_ref }} + continue-on-error: true + - name: Deploy main + if: github.event_name == 'push' + run: | git fetch origin gh-pages mike delete main mike deploy --push main + - name: Deploy branch + if: github.event_name == 'pull_request' + run: | + git fetch origin gh-pages + mike deploy --push ${{ github.head_ref }} diff --git a/docs/_static/tmp_trigger_CI.txt b/docs/_static/tmp_trigger_CI.txt new file mode 100644 index 00000000..0a046902 --- /dev/null +++ b/docs/_static/tmp_trigger_CI.txt @@ -0,0 +1 @@ +trigger1 \ No newline at end of file