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

[Merged by Bors] - fix(data/set/basic): fix name of has_mem.mem.out #13721

Closed
wants to merge 1 commit into from
Closed

[Merged by Bors] - fix(data/set/basic): fix name of has_mem.mem.out #13721

wants to merge 1 commit into from

Conversation

fpvandoorn
Copy link
Member

Open in Gitpod

@fpvandoorn fpvandoorn added easy < 20s of review time. See the lifecycle page for guidelines. awaiting-review The author would like community review of the PR labels Apr 26, 2022
@fpvandoorn fpvandoorn mentioned this pull request Apr 26, 2022
Closed
11 tasks
eric-wieser
eric-wieser approved these changes Apr 26, 2022
View reviewed changes
Copy link
Member

@eric-wieser eric-wieser left a comment

Choose a reason for hiding this comment

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

bors d+

@bors
Copy link

bors bot commented Apr 26, 2022

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

@eric-wieser eric-wieser added the awaiting-CI The author would like to see what CI has to say before doing more work. label Apr 26, 2022
@leanprover-community-bot-assistant leanprover-community-bot-assistant 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 Apr 26, 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 Apr 26, 2022
@eric-wieser
Copy link
Member

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 Apr 26, 2022
bors bot pushed a commit that referenced this pull request Apr 26, 2022
@fpvandoorn
fix(data/set/basic): fix name of has_mem.mem.out (#13721)
48997d7
@bors
Copy link

bors bot commented Apr 27, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title fix(data/set/basic): fix name of has_mem.mem.out [Merged by Bors] - fix(data/set/basic): fix name of has_mem.mem.out Apr 27, 2022
@bors bors bot closed this Apr 27, 2022
@bors bors bot deleted the set_fix branch April 27, 2022 00:04
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Reviewers

@eric-wieser eric-wieser eric-wieser approved these changes

Assignees
No one assigned
Labels
delegated The PR author may merge after reviewing final suggestions. 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
@fpvandoorn @eric-wieser @leanprover-community-bot-assistant