Merge main to release/dev17.11#17038

vzarytovskii merged 10 commits intorelease/dev17.11dotnet/fsharp:release/dev17.11from

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