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

Fix doc_markdown mixed case false positive #3510

Merged
merged 1 commit into from Dec 12, 2018

Conversation

Projects
None yet
3 participants
@phansch
Copy link
Collaborator

phansch commented Dec 7, 2018

Fixes #2343

@phansch phansch closed this Dec 9, 2018

@phansch phansch reopened this Dec 9, 2018

@bors

This comment has been minimized.

Copy link
Contributor

bors commented Dec 12, 2018

☔️ The latest upstream changes (presumably #3533) made this pull request unmergeable. Please resolve the merge conflicts.

@phansch phansch force-pushed the phansch:fix_doc_markdown_mixed_case branch from 6403832 to 785167e Dec 12, 2018

@flip1995

This comment has been minimized.

Copy link
Collaborator

flip1995 commented Dec 12, 2018

bors r+

@flip1995

This comment has been minimized.

Copy link
Collaborator

flip1995 commented Dec 12, 2018

whoops we now need an @ to contact bors 😄

@bors r+ rollup

@bors

This comment has been minimized.

Copy link
Contributor

bors commented Dec 12, 2018

📌 Commit 785167e has been approved by flip1995

@bors

This comment has been minimized.

Copy link
Contributor

bors commented Dec 12, 2018

⌛️ Testing commit 785167e with merge 8a14065...

bors added a commit that referenced this pull request Dec 12, 2018

Auto merge of #3510 - phansch:fix_doc_markdown_mixed_case, r=flip1995
Fix doc_markdown mixed case false positive

Fixes #2343
@bors

This comment has been minimized.

Copy link
Contributor

bors commented Dec 12, 2018

💔 Test failed - status-travis

@bors

This comment has been minimized.

Copy link
Contributor

bors commented Dec 12, 2018

☔️ The latest upstream changes (presumably #3544) made this pull request unmergeable. Please resolve the merge conflicts.

@phansch phansch force-pushed the phansch:fix_doc_markdown_mixed_case branch from 785167e to 7787236 Dec 12, 2018

@phansch

This comment has been minimized.

Copy link
Collaborator

phansch commented Dec 12, 2018

@bors r=flip1995

@bors

This comment has been minimized.

Copy link
Contributor

bors commented Dec 12, 2018

📌 Commit 7787236 has been approved by flip1995

@bors

This comment has been minimized.

Copy link
Contributor

bors commented Dec 12, 2018

⌛️ Testing commit 7787236 with merge 777c909...

bors added a commit that referenced this pull request Dec 12, 2018

Auto merge of #3510 - phansch:fix_doc_markdown_mixed_case, r=flip1995
Fix doc_markdown mixed case false positive

Fixes #2343
@bors

This comment has been minimized.

Copy link
Contributor

bors commented Dec 12, 2018

☀️ Test successful - status-appveyor, status-travis
Approved by: flip1995
Pushing 777c909 to master...

@bors bors merged commit 7787236 into rust-lang:master Dec 12, 2018

3 checks passed

continuous-integration/appveyor/pr AppVeyor build succeeded
Details
continuous-integration/travis-ci/pr The Travis CI build passed
Details
homu Test successful
Details

@phansch phansch deleted the phansch:fix_doc_markdown_mixed_case branch Dec 12, 2018

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment