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: freeze data.bool.basic #17324

Closed
wants to merge 1 commit into from
Closed

[Merged by Bors] - chore: freeze data.bool.basic #17324

wants to merge 1 commit into from

Conversation

kbuzzard
Copy link
Member

@kbuzzard kbuzzard commented Nov 3, 2022

Open in Gitpod

Depends on: the as yet unmerged mathlib4 PR #534 leanprover-community/mathlib4#534

@kbuzzard kbuzzard added blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. mathlib4-synchronization This PR *only* adds a message to the module doc about synchronization with mathlib4 labels Nov 3, 2022
@mathlib-dependent-issues-bot mathlib-dependent-issues-bot removed the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Nov 3, 2022
@kbuzzard kbuzzard changed the title chore: freeze data.sigma.basic chore: freeze data.bool.basic Nov 5, 2022
@semorrison semorrison added blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. awaiting-review The author would like community review of the PR awaiting-author A reviewer has asked the author a question or requested changes and removed blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. awaiting-review The author would like community review of the PR awaiting-author A reviewer has asked the author a question or requested changes labels Nov 5, 2022
@semorrison
Copy link
Collaborator

bors merge

@github-actions github-actions bot added the ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) label Nov 7, 2022
bors bot pushed a commit that referenced this pull request Nov 7, 2022
@kbuzzard
chore: freeze data.bool.basic (#17324)
9eb1e2a
@bors
Copy link

bors bot commented Nov 7, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title chore: freeze data.bool.basic [Merged by Bors] - chore: freeze data.bool.basic Nov 7, 2022
@bors bors bot closed this Nov 7, 2022
@bors bors bot deleted the kbuzzard-freeze-data-bool-basic branch November 7, 2022 06:48
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
mathlib4-synchronization This PR *only* adds a message to the module doc about synchronization with mathlib4 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
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
3 participants
@kbuzzard @semorrison @mathlib-dependent-issues-bot