Merge main to release/dev17.14#18249

psfinaki merged 1 commit intorelease/dev17.14dotnet/fsharp:release/dev17.14from

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