Switch action push trigger from allow-list to ignore-list #4384
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.
PR #4375 limited the github action to run on pushes to specific branches, so as to avoid the double-execution of CI on merge-queue activity (it was triggering on both the
merge_group
event and the merge queue's push to a throwawaygh-readonly-queue/...
branch). Of course we also still trigger on thepull_request
event which fires on any change to a PR.This was a bit too strict. @dmkozh noted that he often likes to push to a branch on his own fork just to get some CI before opening a PR. So my proposed change here switches from an explicit list of branches to trigger the
push
event to an explicit pattern of branches to not trigger thepush
event.(Probably this should wait until the release is done, since if I made a mistake it might disrupt normal operations while figuring it out, @marta-lokhova and/or @SirTyson could you make a note here / merge this PR when you're done?)