chore: trigger CI on doc

aphp · Feb 15, 2024 · fe64062 · fe64062
1 parent 72e2ff4
commit fe64062
Show file tree

Hide file tree

Showing 2 changed files with 16 additions and 1 deletion.
diff --git 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/trigger_CI.txt b/docs/_static/trigger_CI.txt