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

[Merged by Bors] - refactor(*): kill int multiplication diamonds#7255

Closed
sgouezel wants to merge 47 commits intomasterfrom
gsmul_data
Closed

[Merged by Bors] - refactor(*): kill int multiplication diamonds#7255
sgouezel wants to merge 47 commits intomasterfrom
gsmul_data

Conversation

@sgouezel
Copy link
Copy Markdown
Collaborator

@sgouezel sgouezel commented Apr 18, 2021 •
edited by jcommelin
Loading

Insert a data field gsmul in add_comm_group containing a Z-action, and use it to make sure that all diamonds related to Z -actions disappear.

Followup to #7084

Open in Gitpod

@github-actions github-actions bot added the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Apr 18, 2021
@sgouezel sgouezel added help-wanted The author needs attention to resolve issues WIP Work in progress labels Apr 18, 2021
@sgouezel
Copy link
Copy Markdown
Collaborator Author

sgouezel commented Apr 21, 2021

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+`.) merge-conflict Please `git merge origin/master` then a bot will remove this label. and removed awaiting-review The author would like community review of the PR labels Apr 21, 2021
@bryangingechen
Copy link
Copy Markdown
Collaborator

bryangingechen commented Apr 22, 2021

merge conflict
bors r-

@bors
Copy link
Copy Markdown

bors bot commented Apr 22, 2021

Canceled.

@bryangingechen bryangingechen added awaiting-author A reviewer has asked the author a question or requested changes delegated The PR author may merge after reviewing final suggestions. and removed ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) labels Apr 22, 2021
@github-actions github-actions bot removed the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Apr 22, 2021
@github-actions github-actions bot added the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Apr 24, 2021
@github-actions github-actions bot removed the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Apr 24, 2021
@sgouezel
Copy link
Copy Markdown
Collaborator Author

sgouezel commented Apr 25, 2021

bors r+ p=37

bors bot pushed a commit that referenced this pull request Apr 25, 2021
@sgouezel @kim-em
@eric-wieser @digama0
refactor(*): kill int multiplication diamonds (#7255)
8e4ef23 
Insert a data field `gsmul` in `add_comm_group` containing a Z-action, and use it to make sure that all diamonds related to `Z` -actions disappear.

Followup to #7084



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Mario Carneiro <di.gama@gmail.com>
@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-author A reviewer has asked the author a question or requested changes labels Apr 25, 2021
@bors
Copy link
Copy Markdown

bors bot commented Apr 25, 2021

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title refactor(*): kill int multiplication diamonds [Merged by Bors] - refactor(*): kill int multiplication diamonds Apr 25, 2021
@bors bors bot closed this Apr 25, 2021
@bors bors bot deleted the gsmul_data branch April 25, 2021 15:12
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.

Reviewers

3 more reviewers

@eric-wieser eric-wieser eric-wieser left review comments

@kim-em kim-em kim-em approved these changes

@jcommelin jcommelin jcommelin approved these changes

Reviewers whose approvals may not affect merge requirements

Assignees

No one assigned

Labels

delegated The PR author may merge after reviewing final suggestions. 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.

6 participants

@sgouezel @kim-em @jcommelin @bryangingechen @eric-wieser @digama0