From 2566c8a9d8d10da3fbdba19a4dd976f91ca686a7 Mon Sep 17 00:00:00 2001 From: Bryan Gin-ge Chen Date: Sun, 16 Feb 2025 11:41:07 -0500 Subject: [PATCH 1/2] add CI for pull requests Note that this uses the `pull_request` event so it runs the code in the PR branch and does not have access to repo secrets (I don't think there are any relevant ones here though). We need to be extra careful here with external PRs because we run on self-hosted runners. --- .github/workflows/docs.yaml | 2 ++ 1 file changed, 2 insertions(+) diff --git a/.github/workflows/docs.yaml b/.github/workflows/docs.yaml index ca92cc32bfd..c16f2d4ab91 100644 --- a/.github/workflows/docs.yaml +++ b/.github/workflows/docs.yaml @@ -1,6 +1,7 @@ name: build and deploy mathlib4 docs on: + pull_request: workflow_dispatch: schedule: - cron: '0 */8 * * *' # every 8 hours @@ -108,6 +109,7 @@ jobs: path: 'workaround/.lake/build/doc' - name: Deploy to GitHub Pages + if: github.ref == 'refs/heads/main' id: deployment uses: actions/deploy-pages@v4 From a9b86a68cc0a15eb623a35eff77e1166009d8b6d Mon Sep 17 00:00:00 2001 From: Bryan Gin-ge Chen Date: Sun, 16 Feb 2025 18:00:18 -0500 Subject: [PATCH 2/2] Update docs.yaml deploy docs when main is updated --- .github/workflows/docs.yaml | 3 +++ 1 file changed, 3 insertions(+) diff --git a/.github/workflows/docs.yaml b/.github/workflows/docs.yaml index c16f2d4ab91..092d6ef06c9 100644 --- a/.github/workflows/docs.yaml +++ b/.github/workflows/docs.yaml @@ -1,6 +1,9 @@ name: build and deploy mathlib4 docs on: + push: + branches: + - main pull_request: workflow_dispatch: schedule: