Skip to content

[Merged by Bors] - chore: bump to std#260#7134

Closed
kim-em wants to merge 16 commits intomasterfrom
bump_std_260
Closed

[Merged by Bors] - chore: bump to std#260#7134
kim-em wants to merge 16 commits intomasterfrom
bump_std_260

Conversation

@kim-em
Copy link
Copy Markdown
Contributor

@kim-em kim-em commented Sep 13, 2023 •
edited
Loading

@kim-em kim-em added help-wanted The author needs attention to resolve issues WIP Work in progress labels Sep 13, 2023
@ghost ghost added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Sep 13, 2023
@kim-em kim-em added awaiting-review awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. and removed help-wanted The author needs attention to resolve issues WIP Work in progress labels Sep 13, 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 Sep 14, 2023
@ghost ghost added merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) and removed merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) labels Sep 15, 2023
@ghost ghost removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Sep 19, 2023
@ghost ghost added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Sep 19, 2023
@ghost ghost added merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) and removed merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) labels Sep 19, 2023
@ghost ghost removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Sep 27, 2023
@ghost
Copy link
Copy Markdown

ghost commented Sep 27, 2023

This PR/issue depends on:

@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 Sep 27, 2023
@PatrickMassot
Copy link
Copy Markdown
Member

PatrickMassot commented Sep 27, 2023

bors d+

@bors
Copy link
Copy Markdown

bors bot commented Sep 27, 2023

✌️ semorrison 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 This pull request has been delegated to the PR author (or occasionally another non-maintainer). and removed awaiting-review labels Sep 27, 2023
@kim-em
Copy link
Copy Markdown
Contributor Author

kim-em commented Sep 27, 2023

bors merge

@github-actions github-actions bot added the ready-to-merge This PR has been sent to bors. label Sep 27, 2023
bors bot pushed a commit that referenced this pull request Sep 27, 2023
@kim-em @alexkeizer
chore: bump to std#260 (#7134)
2c8d12c 
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Alex Keizer <alex@keizer.dev>
@bors
Copy link
Copy Markdown

bors bot commented Sep 27, 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 chore: bump to std#260 [Merged by Bors] - chore: bump to std#260 Sep 27, 2023
@bors bors bot closed this Sep 27, 2023
@bors bors bot deleted the bump_std_260 branch September 27, 2023 05:02
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

@kim-em @PatrickMassot @alexkeizer