Merge main to release/dev17.12#17450

vzarytovskii merged 2 commits intorelease/dev17.12dotnet/fsharp:release/dev17.12from

merges/main-to-release/dev17.12dotnet/fsharp:merges/main-to-release/dev17.12Copy head branch name to clipboard