diff --git a/.github/workflows/publish_doc.yml b/.github/workflows/publish_doc.yml index bd37883d..cad93a58 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 }} \ No newline at end of file diff --git a/docs/_static/trigger_CI.txt b/docs/_static/trigger_CI.txt new file mode 100644 index 00000000..e69de29b