Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[Merged by Bors] - v2.3.0 #3222

Closed
wants to merge 1 commit into from
Closed

Conversation

paulhauner
Copy link
Member

@paulhauner paulhauner commented May 26, 2022

Issue Addressed

NA

Proposed Changes

Please list or describe the changes introduced by this PR.

Additional Info

NA

@paulhauner paulhauner added the ready-for-review The code is ready for review label May 26, 2022
@paulhauner
Copy link
Member Author

paulhauner commented May 27, 2022

Rebased on staging to include #3223 and #3225.

@paulhauner paulhauner changed the base branch from unstable to stable May 30, 2022 00:15
@paulhauner paulhauner changed the base branch from stable to unstable May 30, 2022 00:15
@paulhauner
Copy link
Member Author

I rebased earlier to remove #3221 which didn't quite make it into unstable on time.

Copy link
Member

@michaelsproul michaelsproul left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Let's go!

bors r+

@michaelsproul michaelsproul added ready-for-merge This PR is ready to merge. and removed ready-for-review The code is ready for review labels May 30, 2022
bors bot pushed a commit that referenced this pull request May 30, 2022
## Issue Addressed

NA

## Proposed Changes

Please list or describe the changes introduced by this PR.

## Additional Info

- Pending testing on our infra. **Please do not merge**
@bors
Copy link

bors bot commented May 30, 2022

Build failed:

@paulhauner
Copy link
Member Author

bors retry

bors bot pushed a commit that referenced this pull request May 30, 2022
## Issue Addressed

NA

## Proposed Changes

Please list or describe the changes introduced by this PR.

## Additional Info

- Pending testing on our infra. **Please do not merge**
@bors bors bot changed the title v2.3.0 [Merged by Bors] - v2.3.0 May 30, 2022
@bors bors bot closed this May 30, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
ready-for-merge This PR is ready to merge.
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants