Skip to content

Conversation

@majocha
Copy link
Contributor

@majocha majocha commented May 21, 2024

Description

Fixes #17205

Checklist

  • Test case added

@majocha majocha requested a review from a team as a code owner May 21, 2024 22:32
@github-actions
Copy link
Contributor

github-actions bot commented May 21, 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

@majocha
Copy link
Contributor Author

majocha commented May 22, 2024

I think this is ready.

@psfinaki
Copy link
Contributor

@ForNeVeR maybe take a look if you have a chance :)

Copy link
Contributor

@ForNeVeR ForNeVeR left a comment

Choose a reason for hiding this comment

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

LGTM. I cannot imagine a scenario when this breaks (so far!)

@vzarytovskii
Copy link
Member

LGTM. I cannot imagine a scenario when this breaks (so far!)

Famous last words, but lgtm too

@vzarytovskii vzarytovskii added the NO_RELEASE_NOTES Label for pull requests which signals, that user opted-out of providing release notes label May 22, 2024
@vzarytovskii
Copy link
Member

/run fantomas

@dotnet dotnet deleted a comment from github-actions bot May 22, 2024
@dotnet dotnet deleted a comment from psfinaki May 22, 2024
@psfinaki
Copy link
Contributor

/azp run

@azure-pipelines
Copy link

Azure Pipelines successfully started running 2 pipeline(s).

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.

MultipleDiagnosticsLoggers.Parallel deadlock

5 participants