Skip to content
This repository has been archived by the owner on Jul 24, 2024. It is now read-only.

[Merged by Bors] - chore(*): update to lean 3.39.2c #12102

Closed
wants to merge 1 commit into from
Closed

[Merged by Bors] - chore(*): update to lean 3.39.2c #12102

wants to merge 1 commit into from

Conversation

gebner
Copy link
Member

@gebner gebner commented Feb 17, 2022

Open in Gitpod

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

bors merge

@bors
Copy link

bors bot commented Feb 17, 2022

👎 Rejected by label

@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-CI The author would like to see what CI has to say before doing more work. awaiting-review The author would like community review of the PR labels Feb 17, 2022
@bryangingechen
Copy link
Collaborator

bors r+

bors bot pushed a commit that referenced this pull request Feb 17, 2022
@gebner
chore(*): update to lean 3.39.2c (#12102)
c9e8c64
@bors
Copy link

bors bot commented Feb 17, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title chore(*): update to lean 3.39.2c [Merged by Bors] - chore(*): update to lean 3.39.2c Feb 17, 2022
@bors bors bot closed this Feb 17, 2022
@bors bors bot deleted the 3392 branch February 17, 2022 18:46
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Reviewers
No reviews
Assignees
No one assigned
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
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@gebner @robertylewis @bryangingechen