-
Notifications
You must be signed in to change notification settings - Fork 710
Fix #9694 Don't imply that Haddock docs exist, when warning not installed #9695
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
Conversation
@mpilgrem we absolutely dropped the ball on this one. Do you want to try to resurrect it? |
eeb76cd
to
971e12a
Compare
@mpilgrem: let's rescue this valuable PR! Let me start by rebasing... |
@mergify rebase |
✅ Branch has been successfully rebased |
CI seems fine. Let me rebase again. @mpilgrem: would you like to set the merge_me label? |
@mergify rebase |
✅ Branch has been successfully rebased |
In the interest of saving this PR, let me set the merge label. |
@mergify reset |
❌ Sorry but I didn't understand the command. Please consult the commands documentation 📚. |
@mergify refresh |
✅ Pull request refreshed |
Oh, it was still some minutes to reach the 2 days delay. We'll see now if comments reset the delay... |
Only if they're on review comments. |
Also the "ready and waiting" label's already on it, so that shouldn't matter. I think it has to be re-queued? |
@Mergifyio queue |
✅ The pull request has been merged automaticallyThe pull request has been merged automatically at c2f046b |
|
Hmm, apparently changelogs are not a required CI job. @geekosaur: shall we make it required? |
Depends on how often this is likely to happen, I guess, although I don't recall seeing it before. Others? @ulysses4ever, @Kleidukos, @ffaf1? |
I don't remember seeing this error before. I'm pro adding 9it as a required job. |
I went ahead and added it. |
Link to issue: #9694