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.

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

Add back reference from constraints to flags #9264

Merged
merged 1 commit into from
Oct 20, 2023

Conversation

philderbeast
Copy link
Collaborator

I saw that flags referenced constraints but not vice-versa in the docs so I added the back reference.

@andreabedini andreabedini self-requested a review October 17, 2023 03:52
@andreabedini andreabedini added the merge me Tell Mergify Bot to merge label Oct 17, 2023
@andreabedini
Copy link
Collaborator

Thank you @philderbeast

@philderbeast
Copy link
Collaborator Author

@andreabedini, is it now OK to hit the green [Merge pull request] button?

@ulysses4ever
Copy link
Collaborator

ulysses4ever commented Oct 18, 2023

@philderbeast we don't merge manually, generally. The bot will take care of it after a mandatory two-days delay.

Thank you for your contribution, as usual!

@philderbeast
Copy link
Collaborator Author

philderbeast commented Oct 18, 2023

Thanks @ulysses4ever. We've had trouble with automated merging of my contributions before and I was wondering if we still need to watch out for this and do it manually, #9043 (comment).

@ulysses4ever
Copy link
Collaborator

ulysses4ever commented Oct 18, 2023

@philderbeast oh, right, thank you for the reminder! Since then, I did implement something that should allow us to use the bot anyways (#9108). It just needs another label: not the standard merge me/merge+squath, but rather merge+no rebase. Let's try it!

The two-days-of-silence delay will automagically be honored this way, presumably.

@ulysses4ever ulysses4ever added merge+no rebase and removed merge me Tell Mergify Bot to merge labels Oct 18, 2023
@mergify mergify bot added the merge delay passed Applied (usually by Mergify) when PR approved and received no updates for 2 days label Oct 20, 2023
@mergify mergify bot merged commit a260cde into haskell:master Oct 20, 2023
43 checks passed
@ulysses4ever
Copy link
Collaborator

And it worked — hooray!

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
merge delay passed Applied (usually by Mergify) when PR approved and received no updates for 2 days merge+no rebase
Projects
None yet
Development

Successfully merging this pull request may close these issues.

4 participants