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.

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

[Merged by Bors] - refactor(data/set/n_ary): extract from data/set/basic #17836

Closed
wants to merge 2 commits into from

Conversation

eric-wieser
Copy link
Member

@eric-wieser eric-wieser commented Dec 6, 2022

This is essentially just a copy paste, with one or two whitespace fixes.

This split is consistent with how finset/n_ary is its own file, and does a nice job of making data/set/basic a bit shorter.

The comment fixes referring to this new file are thanks to #17825.


Open in Gitpod

@eric-wieser eric-wieser 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 Dec 6, 2022
@eric-wieser eric-wieser changed the title refactor(data/set_nary): extract from data/set/basic refactor(data/set/n_ary): extract from data/set/basic Dec 7, 2022
@semorrison
Copy link
Collaborator

bors p=10

bors merge

@bors
Copy link

bors bot commented Dec 7, 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-review The author would like community review of the PR labels Dec 7, 2022
@eric-wieser eric-wieser removed the awaiting-CI The author would like to see what CI has to say before doing more work. label Dec 7, 2022
@eric-wieser
Copy link
Member Author

Bors merge

bors bot pushed a commit that referenced this pull request Dec 7, 2022
This is essentially just a copy paste, with one or two whitespace fixes.

This split is consistent with how `finset/n_ary` is its own file, and does a nice job of making `data/set/basic` a bit shorter.

The comment fixes referring to this new file are thanks to #17825.
@bors
Copy link

bors bot commented Dec 7, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title refactor(data/set/n_ary): extract from data/set/basic [Merged by Bors] - refactor(data/set/n_ary): extract from data/set/basic Dec 7, 2022
@bors bors bot closed this Dec 7, 2022
@bors bors bot deleted the eric-wieser/set.n_ary branch December 7, 2022 04:15
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
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.

None yet

2 participants