Merge release/dev17.12 to release/dev17.13#17850

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

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