Skip to content

[Merged by Bors] - fix: precedence of ⁺, ⁻ and abs#5619

Closed
fpvandoorn wants to merge 7 commits intomasterfrom
pospart_prec
Closed

[Merged by Bors] - fix: precedence of ⁺, ⁻ and abs#5619
fpvandoorn wants to merge 7 commits intomasterfrom
pospart_prec

Conversation

@fpvandoorn
Copy link
Copy Markdown
Member

@fpvandoorn fpvandoorn commented Jun 30, 2023

Open in Gitpod

@fpvandoorn fpvandoorn added awaiting-review awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. labels Jun 30, 2023
@fpvandoorn fpvandoorn changed the title fix: precedence of ⁺ and ⁻ fix: precedence of ⁺, ⁻ and abs Jun 30, 2023
@github-actions github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Jun 30, 2023
@ocfnash
Copy link
Copy Markdown
Contributor

ocfnash commented Jul 2, 2023

And again, thanks!

bors merge

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Jul 2, 2023
@bors
Copy link
Copy Markdown

bors bot commented Jul 2, 2023

Merge conflict.

@ocfnash
Copy link
Copy Markdown
Contributor

ocfnash commented Jul 2, 2023

bors d+

@bors
Copy link
Copy Markdown

bors bot commented Jul 2, 2023

✌️ fpvandoorn 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 the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Jul 2, 2023
@kim-em kim-em added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jul 2, 2023
@kim-em kim-em removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jul 2, 2023
@fpvandoorn
Copy link
Copy Markdown
Member Author

fpvandoorn commented Jul 2, 2023

bors merge

bors bot pushed a commit that referenced this pull request Jul 2, 2023
@fpvandoorn
fix: precedence of ⁺, ⁻ and abs (#5619)
6c1021b
@bors
Copy link
Copy Markdown

bors bot commented Jul 2, 2023

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

@bors bors bot changed the title fix: precedence of ⁺, ⁻ and abs [Merged by Bors] - fix: precedence of ⁺, ⁻ and abs Jul 2, 2023
@bors bors bot closed this Jul 2, 2023
@bors bors bot deleted the pospart_prec branch July 2, 2023 15:03
kbuzzard pushed a commit that referenced this pull request Jul 6, 2023
@fpvandoorn @kbuzzard
fix: precedence of ⁺, ⁻ and abs (#5619)
817d9a4
kim-em pushed a commit that referenced this pull request Aug 14, 2023
@fpvandoorn @kim-em
fix: precedence of ⁺, ⁻ and abs (#5619)
442e70a
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). ready-to-merge This PR has been sent to bors.

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@fpvandoorn @ocfnash @kim-em