Enable github CI for all (including external) PRs #375
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Currently, our github CI doesn't run for PRs from forked repos, e.g. for this one:
#349
This hopefully fixes that.
I think we still have to manually approve CI runs from external forks. But that seems sensible for now.
Update: I first tried out
on: [push, pull_request]
, but that means that for internal PRs we always get duplicated runs, since they're both a PR and a push to a local branch. I changed the config to now:main
branch, andBut this means that we won't get CI runs for pushes to branches other then
main
in this repo, if there's no PR open for that branch. So if you want a CI run, you'd have to open a PR (possibly a draft PR). I think this is acceptable. WDYT?