Skip to content

[Merged by Bors] - fix: change compl precedence#5586

Closed
fpvandoorn wants to merge 8 commits intomasterfrom
compl_prec
Closed

[Merged by Bors] - fix: change compl precedence#5586
fpvandoorn wants to merge 8 commits intomasterfrom
compl_prec

Conversation

@fpvandoorn
Copy link
Copy Markdown
Member


Open in Gitpod

@fpvandoorn fpvandoorn added awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. WIP Work in progress labels Jun 29, 2023
@fpvandoorn fpvandoorn added awaiting-review and removed WIP Work in progress labels Jun 29, 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 Jun 29, 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 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
@kim-em
Copy link
Copy Markdown
Contributor

kim-em commented Jun 30, 2023

bors merge

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Jun 30, 2023
bors bot pushed a commit that referenced this pull request Jun 30, 2023



Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
@bors
Copy link
Copy Markdown

bors bot commented Jun 30, 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: change compl precedence [Merged by Bors] - fix: change compl precedence Jun 30, 2023
@bors bors bot closed this Jun 30, 2023
@bors bors bot deleted the compl_prec branch June 30, 2023 03:05
kbuzzard pushed a commit that referenced this pull request Jul 6, 2023



Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
kim-em pushed a commit that referenced this pull request Aug 14, 2023



Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

ready-to-merge This PR has been sent to bors.

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants