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

[Merged by Bors] - chore: change from plural to singular in porting notes #10761

Closed
wants to merge 1 commit into from
Closed

[Merged by Bors] - chore: change from plural to singular in porting notes #10761

wants to merge 1 commit into from

Conversation

pitmonticone
Copy link
Collaborator

@pitmonticone pitmonticone commented Feb 20, 2024 •
edited by mathlib-bors bot

No description provided.

@pitmonticone pitmonticone added awaiting-review The author would like community review of the PR easy < 20s of review time. See the lifecycle page for guidelines. porting-notes Mathlib3 to Mathlib4 porting notes. labels Feb 20, 2024
Vierkantor
Vierkantor approved these changes Feb 20, 2024
View reviewed changes
Copy link
Contributor

@Vierkantor Vierkantor left a comment

Choose a reason for hiding this comment

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

Thanks! This looks good to me, assuming there is no conflict with your other PRs.

bors d+

@mathlib-bors
Copy link

mathlib-bors bot commented Feb 20, 2024

✌️ pitmonticone can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added delegated and removed awaiting-review The author would like community review of the PR labels Feb 20, 2024
@pitmonticone
Copy link
Collaborator Author

Thanks! This looks good to me, assuming there is no conflict with your other PRs.

Thank you for your review @Vierkantor! No, there shouldn't be any conflict.

@pitmonticone
Copy link
Collaborator Author

bors r+

mathlib-bors bot pushed a commit that referenced this pull request Feb 20, 2024
@pitmonticone
chore: change from plural to singular in porting notes (#10761)
0f21e51
@mathlib-bors
Copy link

mathlib-bors bot commented Feb 20, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title chore: change from plural to singular in porting notes [Merged by Bors] - chore: change from plural to singular in porting notes Feb 20, 2024
@mathlib-bors mathlib-bors bot closed this Feb 20, 2024
@mathlib-bors mathlib-bors bot deleted the pitmonticone/singular branch February 20, 2024 19:12
thorimur pushed a commit that referenced this pull request Feb 24, 2024
@pitmonticone @thorimur
chore: change from plural to singular in porting notes (#10761)
54374c4
thorimur pushed a commit that referenced this pull request Feb 26, 2024
@pitmonticone @thorimur
chore: change from plural to singular in porting notes (#10761)
304ee1c
riccardobrasca pushed a commit that referenced this pull request Mar 1, 2024
@pitmonticone @riccardobrasca
chore: change from plural to singular in porting notes (#10761)
398ea26
dagurtomas pushed a commit that referenced this pull request Mar 22, 2024
@pitmonticone @dagurtomas
chore: change from plural to singular in porting notes (#10761)
3cce1ed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@Vierkantor Vierkantor Vierkantor approved these changes

Assignees
No one assigned
Labels
delegated easy < 20s of review time. See the lifecycle page for guidelines. porting-notes Mathlib3 to Mathlib4 porting notes.
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
3 participants
@pitmonticone @Vierkantor @leanprover-community-mathlib4-bot