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

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

vzarytovskii merged 2 commits into

release/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