Skip to content

[Merged by Bors] - chore: bump toolchain to v4.2.0-rc1#7370

Closed
kim-em wants to merge 3 commits intomasterfrom
bump-v4.2.0-rc1
Closed

[Merged by Bors] - chore: bump toolchain to v4.2.0-rc1#7370
kim-em wants to merge 3 commits intomasterfrom
bump-v4.2.0-rc1

Conversation

@kim-em
Copy link
Copy Markdown
Contributor

@kim-em kim-em commented Sep 26, 2023

This rolls in the changed from #6928.

Co-authored-by: Thomas Murrills thomasmurrills@gmail.com


Open in Gitpod

@ghost ghost added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Sep 26, 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 26, 2023
@ghost
Copy link
Copy Markdown

ghost commented Sep 26, 2023

This PR/issue depends on:

@kim-em kim-em added the auto-merge-after-CI Please do not add manually. Requests for a bot to merge automatically once CI is done. label Sep 26, 2023
@ghost
Copy link
Copy Markdown

ghost commented Sep 26, 2023

As this PR is labelled auto-merge-after-CI, we are now sending it to bors:

bors merge

bors bot pushed a commit that referenced this pull request Sep 26, 2023
This rolls in the changed from #6928.

Co-authored-by: Thomas Murrills <thomasmurrills@gmail.com>



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
@bors
Copy link
Copy Markdown

bors bot commented Sep 26, 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 toolchain to v4.2.0-rc1 [Merged by Bors] - chore: bump toolchain to v4.2.0-rc1 Sep 26, 2023
@bors bors bot closed this Sep 26, 2023
@bors bors bot deleted the bump-v4.2.0-rc1 branch September 26, 2023 11:46
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

auto-merge-after-CI Please do not add manually. Requests for a bot to merge automatically once CI is done.

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant