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

[Merged by Bors] - chore(topology): add 2 missing inhabited instances #10446

Closed
wants to merge 1 commit into from

Conversation

urkud
Copy link
Member

@urkud urkud commented Nov 24, 2021

Also add an instance from discrete_topology to topological_ring.


Open in Gitpod

Also add an instance from `discrete_topology` to `topological_ring`.
@urkud urkud added awaiting-review The author would like community review of the PR awaiting-CI The author would like to see what CI has to say before doing more work. labels Nov 24, 2021
@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 Nov 24, 2021
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

@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 Nov 24, 2021
bors bot pushed a commit that referenced this pull request Nov 24, 2021
Also add an instance from `discrete_topology` to `topological_ring`.
@bors
Copy link

bors bot commented Nov 24, 2021

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title chore(topology): add 2 missing inhabited instances [Merged by Bors] - chore(topology): add 2 missing inhabited instances Nov 24, 2021
@bors bors bot closed this Nov 24, 2021
@bors bors bot deleted the YK-top-inhab branch November 24, 2021 07:49
ericrbg pushed a commit that referenced this pull request Nov 24, 2021
Also add an instance from `discrete_topology` to `topological_ring`.
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Labels
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
Development

Successfully merging this pull request may close these issues.

2 participants