Skip to content

Conversation

@majocha
Copy link
Contributor

@majocha majocha commented Feb 15, 2024

See potential problem here: #16576 (comment)

The API could be better, but it works.

I think no release notes needed.

@majocha majocha requested a review from a team as a code owner February 15, 2024 14:33
@github-actions
Copy link
Contributor

github-actions bot commented Feb 15, 2024

⚠️ Release notes required, but author opted out

Warning

Author opted out of release notes, check is disabled for this pull request.
cc @dotnet/fsharp-team-msft

@0101 0101 added the NO_RELEASE_NOTES Label for pull requests which signals, that user opted-out of providing release notes label Feb 15, 2024
Copy link
Contributor

@psfinaki psfinaki left a comment

Choose a reason for hiding this comment

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

Thanks Jakub!

@psfinaki psfinaki enabled auto-merge (squash) February 16, 2024 12:57
@psfinaki psfinaki merged commit 0f520bc into dotnet:main Feb 16, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

NO_RELEASE_NOTES Label for pull requests which signals, that user opted-out of providing release notes

Projects

Archived in project

Development

Successfully merging this pull request may close these issues.

3 participants