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

[Merged by Bors] - split(data/psigma/order): Split off order.lexicographic#10953

Closed
YaelDillies wants to merge 4 commits intomasterfrom
move_psigma_order
Closed

[Merged by Bors] - split(data/psigma/order): Split off order.lexicographic#10953
YaelDillies wants to merge 4 commits intomasterfrom
move_psigma_order

Conversation

@YaelDillies
Copy link
Copy Markdown
Collaborator

This moves all the stuff about Σ' i, α i to a new file data.psigma.order. This mimics the file organisation of sigma.

I'm crediting:


Open in Gitpod

@YaelDillies YaelDillies added the awaiting-review The author would like community review of the PR label Dec 21, 2021
Copy link
Copy Markdown
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+

Let's capture why these are currently instances in the docstring, even if the argument is less good than the original authors thought it was.

@bors
Copy link
Copy Markdown

bors bot commented Dec 21, 2021

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

@github-actions github-actions bot 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 Dec 21, 2021
@YaelDillies
Copy link
Copy Markdown
Collaborator Author

bors merge

bors bot pushed a commit that referenced this pull request Dec 22, 2021
This moves all the stuff about `Σ' i, α i` to a new file `data.psigma.order`. This mimics the file organisation of `sigma`.

I'm crediting:
* Scott for #820
* Minchao for #914
@bors
Copy link
Copy Markdown

bors bot commented Dec 23, 2021

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title split(data/psigma/order): Split off order.lexicographic [Merged by Bors] - split(data/psigma/order): Split off order.lexicographic Dec 23, 2021
@bors bors bot closed this Dec 23, 2021
@bors bors bot deleted the move_psigma_order branch December 23, 2021 00:55
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.

Labels

delegated The PR author may merge after reviewing final suggestions.

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants