diff options
| author | Florian Bruhin <me@the-compiler.org> | 2021-01-26 18:35:38 +0100 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-01-26 17:35:38 +0000 |
| commit | 4487c16c8e72c24d62da589a7bf7c1e3666013a6 (patch) | |
| tree | d3267a00a03391da0170a931649f9f59eb708e77 /.github/workflows/ci.yml | |
| parent | 4555a608946d7ecee68082b1c5cdde2557ba4455 (diff) | |
ci: Run on pull requests (#27)
Right now the CI is configured to only run on pushes (to this repository), but not on PRs (from another repository).
The downside of this is that PRs for a branch in this repository will run twice. If you only push directly to e.g. master, it might be worth adjusting that - also see https://github.community/t/how-to-trigger-an-action-on-push-or-pull-request-but-not-both/16662
Diffstat (limited to '.github/workflows/ci.yml')
| -rw-r--r-- | .github/workflows/ci.yml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index c4179e4..61042a8 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml | |||
| @@ -4,6 +4,7 @@ on: | |||
| 4 | release: | 4 | release: |
| 5 | types: [created] | 5 | types: [created] |
| 6 | push: | 6 | push: |
| 7 | pull_request: | ||
| 7 | schedule: | 8 | schedule: |
| 8 | # Runs every Thursday at 20:23 GMT to avoid bit rot | 9 | # Runs every Thursday at 20:23 GMT to avoid bit rot |
| 9 | - cron: "20 23 * * 4" | 10 | - cron: "20 23 * * 4" |