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: remove 4 porting notes about continuity #12358

Closed
wants to merge 1 commit into from
Closed

[Merged by Bors] - chore: remove 4 porting notes about continuity #12358

wants to merge 1 commit into from

Conversation

adomani
Copy link
Collaborator

@adomani adomani commented Apr 23, 2024

Open in Gitpod

@adomani adomani added awaiting-review The author would like community review of the PR porting-notes Mathlib3 to Mathlib4 porting notes. labels Apr 23, 2024
grunweg
grunweg approved these changes Apr 23, 2024
View reviewed changes
Copy link
Collaborator

@grunweg grunweg left a comment

Choose a reason for hiding this comment

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

Straightforward; I like this. Thank you for doing this!

@loefflerd
Copy link
Collaborator

Thanks!

maintainer merge

@github-actions GitHub Actions
Copy link

🚀 Pull request has been placed on the maintainer queue by loefflerd.

jcommelin
jcommelin approved these changes Apr 23, 2024
View reviewed changes
Copy link
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

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

Thanks 🎉

bors merge

@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review The author would like community review of the PR labels Apr 23, 2024
mathlib-bors bot pushed a commit that referenced this pull request Apr 23, 2024
@adomani
chore: remove 4 porting notes about continuity (#12358)
b57f05f
@mathlib-bors
Copy link

mathlib-bors bot commented Apr 23, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title chore: remove 4 porting notes about continuity [Merged by Bors] - chore: remove 4 porting notes about continuity Apr 23, 2024
@mathlib-bors mathlib-bors bot closed this Apr 23, 2024
@mathlib-bors mathlib-bors bot deleted the adomani/porting_note_continuity branch April 23, 2024 11:20
Jun2M pushed a commit that referenced this pull request Apr 24, 2024
@adomani @Jun2M
chore: remove 4 porting notes about continuity (#12358)
3aec0a2
callesonne pushed a commit that referenced this pull request May 16, 2024
@adomani @callesonne
chore: remove 4 porting notes about continuity (#12358)
eb6ddf5
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@jcommelin jcommelin jcommelin approved these changes

@grunweg grunweg grunweg approved these changes

Assignees
No one assigned
Labels
maintainer-merge porting-notes Mathlib3 to Mathlib4 porting notes. ready-to-merge This PR has been sent to bors.
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
5 participants
@adomani @loefflerd @jcommelin @grunweg @leanprover-community-mathlib4-bot