Skip to content

Use ref instead head_ref to cancelling jobs #8013

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 1 commit into from
Feb 24, 2022

Conversation

jneira
Copy link
Member

@jneira jneira commented Feb 24, 2022

As per @fgaz question here: #8000 (comment)

Rationale

Good point head_ref is only defined for pull requests and workflows are triggered for direct commits too.
The consequence is that, for consecutive direct and merge commits in master (and 3.6, 3.4 etc), they will be cancelled but the last one.
So we will lose the status of those intermmediate commits.
There is a small probability of a green pr breaking master cause we are not enforcing the pr is up to date with master before merging it. Also there is a even small probability of merge another pr just after the offending one and we will not know the real cause is the intemmediate and no the final one.


Please include the following checklist in your PR:

Please also shortly describe how you tested your change. Bonus points for added tests!

@jneira jneira requested a review from fgaz February 24, 2022 10:24
Copy link
Member

@fgaz fgaz left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks!

@jneira jneira added the merge me Tell Mergify Bot to merge label Feb 24, 2022
@mergify mergify bot merged commit b5f8913 into haskell:master Feb 24, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
merge me Tell Mergify Bot to merge
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants