Skip to content

[Merged by Bors] - fix: minor changes in Groups/Defs#719

Closed
fpvandoorn wants to merge 1 commit intomasterfrom
defsfixes
Closed

[Merged by Bors] - fix: minor changes in Groups/Defs#719
fpvandoorn wants to merge 1 commit intomasterfrom
defsfixes

Conversation

@fpvandoorn
Copy link
Copy Markdown
Member

@fpvandoorn fpvandoorn commented Nov 24, 2022 •
edited
Loading

@kim-em
Copy link
Copy Markdown
Contributor

kim-em commented Nov 24, 2022

bors merge

bors bot pushed a commit that referenced this pull request Nov 24, 2022
@fpvandoorn
fix: minor changes in Groups/Defs (#719)
c174706 
* Remove instance and add `to_additive`
* Point some comments to the right issue
* Resolves the issue in #707
* Might conflict with #717
@bors
Copy link
Copy Markdown

bors bot commented Nov 24, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title fix: minor changes in Groups/Defs [Merged by Bors] - fix: minor changes in Groups/Defs Nov 24, 2022
@bors bors bot closed this Nov 24, 2022
@bors bors bot deleted the defsfixes branch November 24, 2022 18:43
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@Ruben-VandeVelde Ruben-VandeVelde Ruben-VandeVelde approved these changes

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@fpvandoorn @kim-em @Ruben-VandeVelde