chore: Trigger doc CI on PR

.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 }}

docs/_static/tmp_trigger_CI.txt

@@ -0,0 +1 @@
+trigger1