Skip to content

Commit f9ac5d9

Browse files
add CI for pull requests, deploy docs when main is updated (#7)
* 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. * Update docs.yaml deploy docs when main is updated
1 parent 1761c19 commit f9ac5d9

File tree

1 file changed

+5
-0
lines changed

1 file changed

+5
-0
lines changed

.github/workflows/docs.yaml

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,10 @@
11
name: build and deploy mathlib4 docs
22

33
on:
4+
push:
5+
branches:
6+
- main
7+
pull_request:
48
workflow_dispatch:
59
schedule:
610
- cron: '0 */8 * * *' # every 8 hours
@@ -108,6 +112,7 @@ jobs:
108112
path: 'workaround/.lake/build/doc'
109113

110114
- name: Deploy to GitHub Pages
115+
if: github.ref == 'refs/heads/main'
111116
id: deployment
112117
uses: actions/deploy-pages@v4
113118

0 commit comments

Comments
 (0)