Skip to content

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

Closed
pitmonticone wants to merge 1 commit intomasterfrom
pitmonticone/singular
Closed

[Merged by Bors] - chore: change from plural to singular in porting notes#10761
pitmonticone wants to merge 1 commit intomasterfrom
pitmonticone/singular

Conversation

@pitmonticone
Copy link
Copy Markdown
Member

@pitmonticone pitmonticone commented Feb 20, 2024

No description provided.

@pitmonticone pitmonticone added awaiting-review easy < 20s of review time. See the lifecycle page for guidelines. porting-notes Mathlib3 to Mathlib4 porting notes. labels Feb 20, 2024
Copy link
Copy Markdown
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
Copy Markdown
Contributor

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.

@ghost ghost added delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). and removed awaiting-review labels Feb 20, 2024
@pitmonticone
Copy link
Copy Markdown
Member 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
Copy Markdown
Member Author

bors r+

@mathlib-bors
Copy link
Copy Markdown
Contributor

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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). easy < 20s of review time. See the lifecycle page for guidelines. porting-notes Mathlib3 to Mathlib4 porting notes.

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants