Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
ci: enable CI on all pushes except merge queue
Every push really should have CI. The only reason we didn't was to avoid duplicating CI for the merge queue; looks like there's a better way to do that. This uses https://docs.github.com/en/actions/using-workflows/workflow-syntax-for-github-actions#onpushbranchestagsbranches-ignoretags-ignore to ignore merge queue branches. Test plan: check that opening a github PR with this change triggers CI, but that CI is labelled as "push" CI, then check that after merge, the merge queue doesn't duplicate CI, and gerrit's branches trigger CI without a PR. Change-Id: Id2d8bdb0b670d6906576878884844dbb64d8eb16
- Loading branch information