Skip to content
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.

Sign up for GitHub

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

Jump to bottom

Make circleci honour [skip ci] wherever is placed in the pr info (title, description) #2289

Merged
merged 7 commits into from Oct 22, 2021
Merged

Make circleci honour [skip ci] wherever is placed in the pr info (title, description) #2289

merged 7 commits into from Oct 22, 2021

Conversation

jneira
Copy link
Member

@jneira jneira commented Oct 21, 2021 •
edited

michaelpj
michaelpj approved these changes Oct 22, 2021
View reviewed changes
Copy link
Collaborator

@michaelpj michaelpj left a comment

Choose a reason for hiding this comment

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

If it's an ugly hack with caveats, maybe include a comment explaining it and what the caveats are?

@jneira
Copy link
Member Author

jneira commented Oct 22, 2021

If it's an ugly hack with caveats, maybe include a comment explaining it and what the caveats are?

Not sure about what can they be, that is the worst news 😝

The string [skip ci] is hard to collide with any other meaningful info from the raw json, i think so maybe it would not have any serious problem in practice

@jneira jneira added the merge me Label to trigger pull request merge label Oct 22, 2021
@mergify mergify bot merged commit d44a706 into haskell:master Oct 22, 2021
@jneira jneira mentioned this pull request Oct 24, 2021
Merged
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@michaelpj michaelpj michaelpj approved these changes

@Ailrun Ailrun Awaiting requested review from Ailrun

@pepeiborra pepeiborra Awaiting requested review from pepeiborra

Assignees
No one assigned
Labels
merge me Label to trigger pull request merge
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
2 participants
@jneira @michaelpj