Skip to content

[Merged by Bors] - chore: bump to nightly-2022-12-13#999

Closed
kim-em wants to merge 1 commit intomasterfrom
nightly-2022-12-13
Closed

[Merged by Bors] - chore: bump to nightly-2022-12-13#999
kim-em wants to merge 1 commit intomasterfrom
nightly-2022-12-13

Conversation

@kim-em
Copy link
Copy Markdown
Contributor

@kim-em kim-em commented Dec 14, 2022

No description provided.

@kim-em
Copy link
Copy Markdown
Contributor Author

kim-em commented Dec 14, 2022

bors merge

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Dec 14, 2022
bors bot pushed a commit that referenced this pull request Dec 14, 2022
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
@bors
Copy link
Copy Markdown

bors bot commented Dec 14, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title chore: bump to nightly-2022-12-13 [Merged by Bors] - chore: bump to nightly-2022-12-13 Dec 14, 2022
@bors bors bot closed this Dec 14, 2022
@bors bors bot deleted the nightly-2022-12-13 branch December 14, 2022 03:23
bors bot pushed a commit that referenced this pull request Dec 14, 2022
- [x] depends on: #999 

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
bors bot pushed a commit that referenced this pull request Dec 14, 2022
- [x] depends on: #999 

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
bors bot pushed a commit that referenced this pull request Dec 14, 2022
- [x] depends on: #999 

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
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.

1 participant