Skip to content

Conversation

@elachlan
Copy link
Contributor

@elachlan elachlan commented Jan 12, 2022

Copy link
Member

@ladipro ladipro left a comment

Choose a reason for hiding this comment

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

Thank you!

@elachlan
Copy link
Contributor Author

@rainersigwald I think this is ready to merge.

@rainersigwald rainersigwald added the merge-when-branch-open PRs that are approved, except that there is a problem that means we are not merging stuff right now. label Jan 19, 2022
@ladipro ladipro merged commit 0dedd95 into dotnet:main Jan 24, 2022
@elachlan elachlan deleted the SA1302 branch January 24, 2022 11:38
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

merge-when-branch-open PRs that are approved, except that there is a problem that means we are not merging stuff right now.

Projects

None yet

Development

Successfully merging this pull request may close these issues.

4 participants