github_workflows: clean up workflow

- rename workflow file to better reflect current state - only deploy on push event (Fixes google#1742) PiperOrigin-RevId: 698950685
antmicro · Nov 22, 2024 · 507358c · 507358c
1 parent 29dca2e
commit 507358c
Showing 1 changed file with 1 addition and 0 deletions.
diff --git a/...ub/workflows/build-mkdocs-commit-html.yml → .../workflows/continuous-docs-deployment.yml b/...ub/workflows/build-mkdocs-commit-html.yml → .../workflows/continuous-docs-deployment.yml
@@ -41,6 +41,7 @@ jobs:
     runs-on:
       labels: ubuntu-22.04-4core
     needs: build
+    if: github.event_name == 'push'
     steps:
       - name: Deploy to GitHub Pages
         id: deployment