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

[Merged by Bors] - fix(*): fix typos I made yesterday #15627

Closed
wants to merge 3 commits into from
Closed

Conversation

urkud
Copy link
Member

@urkud urkud commented Jul 22, 2022

Fix 4 typos I made yesterday.


Open in Gitpod

@urkud urkud added easy < 20s of review time. See the lifecycle page for guidelines. awaiting-review The author would like community review of the PR awaiting-CI The author would like to see what CI has to say before doing more work. labels Jul 22, 2022
@PatrickMassot
Copy link
Member

bors d+

@bors
Copy link

bors bot commented Jul 22, 2022

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

@github-actions github-actions bot added delegated The PR author may merge after reviewing final suggestions. and removed awaiting-review The author would like community review of the PR labels Jul 22, 2022
@urkud urkud changed the title fix(data/set/intervals): fix a name fix(*): fix typos I made yesterday Jul 22, 2022
@urkud
Copy link
Member Author

urkud commented Jul 22, 2022

@PatrickMassot , I fixed more typos. Could you please have another look?
bors d-

@urkud urkud added awaiting-review The author would like community review of the PR and removed delegated The PR author may merge after reviewing final suggestions. labels Jul 22, 2022
@github-actions github-actions bot removed the awaiting-review The author would like community review of the PR label Jul 22, 2022
@urkud urkud added the awaiting-review The author would like community review of the PR label Jul 22, 2022
@github-actions github-actions bot removed the awaiting-CI The author would like to see what CI has to say before doing more work. label Jul 23, 2022
@PatrickMassot
Copy link
Member

bors merge

@github-actions github-actions bot added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels Jul 23, 2022
bors bot pushed a commit that referenced this pull request Jul 23, 2022
Fix 4 typos I made yesterday.
@bors
Copy link

bors bot commented Jul 23, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title fix(*): fix typos I made yesterday [Merged by Bors] - fix(*): fix typos I made yesterday Jul 23, 2022
@bors bors bot closed this Jul 23, 2022
@bors bors bot deleted the YK-fix-name branch July 23, 2022 21:26
bottine pushed a commit to bottine/mathlib that referenced this pull request Jul 30, 2022
robertylewis pushed a commit that referenced this pull request Aug 2, 2022
Fix 4 typos I made yesterday.
khwilson pushed a commit that referenced this pull request Aug 2, 2022
Fix 4 typos I made yesterday.
ocfnash pushed a commit to leanprover-community/sphere-eversion that referenced this pull request Aug 9, 2022
Most of the changes from the following Mathlib PRs:
leanprover-community/mathlib#15619 chore(*): Rename normed_group to normed_add_comm_group
leanprover-community/mathlib#15625 refactor(*): rename nondiscrete_normed_field
leanprover-community/mathlib#15632 feat(order/filter/*): filter.pi is countably generated
leanprover-community/mathlib#15634 feat(topology/metric_space/lipschitz): add several lemmas
leanprover-community/mathlib#15627 fix(*): fix typos I made yesterday
leanprover-community/mathlib#15523 feat(geometry/manifold/smooth_manifold_with_corners): properties to prove smoothness of mfderiv
leanprover-community/mathlib#15640 chore(topology/locally_finite): move from topology.basic
ocfnash added a commit to leanprover-community/sphere-eversion that referenced this pull request Sep 12, 2022
Most of the changes from the following Mathlib PRs:
leanprover-community/mathlib#15619 chore(*): Rename normed_group to normed_add_comm_group
leanprover-community/mathlib#15625 refactor(*): rename nondiscrete_normed_field
leanprover-community/mathlib#15632 feat(order/filter/*): filter.pi is countably generated
leanprover-community/mathlib#15634 feat(topology/metric_space/lipschitz): add several lemmas
leanprover-community/mathlib#15627 fix(*): fix typos I made yesterday
leanprover-community/mathlib#15523 feat(geometry/manifold/smooth_manifold_with_corners): properties to prove smoothness of mfderiv
leanprover-community/mathlib#15640 chore(topology/locally_finite): move from topology.basic
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
easy < 20s of review time. See the lifecycle page for guidelines. ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.)
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

2 participants