Cherry-pick #13313 to 17.2 (#13399)#13412

vzarytovskii merged 1 commit intomaindotnet/fsharp:mainfrom

merges/release/dev17.2-to-maindotnet/fsharp:merges/release/dev17.2-to-mainCopy head branch name to clipboard