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

Update docs for an operator #17427

Merged
merged 1 commit into from
Jul 27, 2024
Merged

Update docs for an operator #17427

merged 1 commit into from
Jul 27, 2024

Conversation

psfinaki
Copy link
Member

🤦

@psfinaki psfinaki requested a review from a team as a code owner July 22, 2024 18:16
Copy link
Contributor

github-actions bot commented Jul 22, 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

@psfinaki psfinaki added the NO_RELEASE_NOTES Label for pull requests which signals, that user opted-out of providing release notes label Jul 22, 2024
@psfinaki psfinaki enabled auto-merge (squash) July 23, 2024 15:06
@psfinaki psfinaki closed this Jul 23, 2024
auto-merge was automatically disabled July 23, 2024 15:06

Pull request was closed

@psfinaki psfinaki reopened this Jul 23, 2024
@psfinaki
Copy link
Member Author

/azp run

Copy link

Azure Pipelines successfully started running 2 pipeline(s).

@T-Gro T-Gro enabled auto-merge (squash) July 26, 2024 11:54
@vzarytovskii vzarytovskii merged commit 13c658f into main Jul 27, 2024
32 of 33 checks passed
@psfinaki psfinaki deleted the psfinaki-patch-5 branch July 29, 2024 12:03
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.

4 participants