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

[Merged by Bors] - feat(topology/order): discrete_topology_bot #6163

Closed
wants to merge 2 commits into from
Closed

[Merged by Bors] - feat(topology/order): discrete_topology_bot #6163

wants to merge 2 commits into from

Conversation

jcommelin
Copy link
Member

From lean-liquid

@jcommelin jcommelin added awaiting-review The author would like community review of the PR easy < 20s of review time. See the lifecycle page for guidelines. labels Feb 10, 2021
@fpvandoorn
Copy link
Member

bors r+

@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 Feb 10, 2021
bors bot pushed a commit that referenced this pull request Feb 11, 2021
@jcommelin
feat(topology/order): discrete_topology_bot (#6163)
954ae6a 
From `lean-liquid`
@bors
Copy link

bors bot commented Feb 11, 2021

Canceled.

@robertylewis
Copy link
Member

bors r+

bors bot pushed a commit that referenced this pull request Feb 11, 2021
@jcommelin
feat(topology/order): discrete_topology_bot (#6163)
58632ac 
From `lean-liquid`
@bors
Copy link

bors bot commented Feb 11, 2021

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(topology/order): discrete_topology_bot [Merged by Bors] - feat(topology/order): discrete_topology_bot Feb 11, 2021
@bors bors bot closed this Feb 11, 2021
@bors bors bot deleted the discrete-bot branch February 11, 2021 14:26
jcommelin added a commit that referenced this pull request Feb 11, 2021
@jcommelin
feat(topology/order): discrete_topology_bot (#6163)
78f0d53 
From `lean-liquid`
b-mehta pushed a commit that referenced this pull request Apr 2, 2021
@jcommelin @b-mehta
feat(topology/order): discrete_topology_bot (#6163)
985a862 
From `lean-liquid`
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
@jcommelin @fpvandoorn @robertylewis