From af4e1c9a91e2304ba5c80256af10f5a1e4c7e6c1 Mon Sep 17 00:00:00 2001
From: Sergey Tepliakov <seteplia@microsoft.com>
Date: Fri, 20 Nov 2015 08:59:42 -0800
Subject: [PATCH] Fix for a build break.

---
 Microsoft.Research/Contracts/MsCorlib/System.IO.Path.cs | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Microsoft.Research/Contracts/MsCorlib/System.IO.Path.cs b/Microsoft.Research/Contracts/MsCorlib/System.IO.Path.cs
index b6bb5b45..0bae2087 100644
--- a/Microsoft.Research/Contracts/MsCorlib/System.IO.Path.cs
+++ b/Microsoft.Research/Contracts/MsCorlib/System.IO.Path.cs
@@ -216,8 +216,8 @@ public static string GetRandomFileName()
 
     public static string GetTempFileName()
     {
-      Contract.Ensures(!string.IsNullOrWhitespace(Contract.Result<string>()));
-      Contract.Ensures(Contract.Result<string>().Length >= 4);
+      Contract.Ensures(Contract.Result<string>() != null);
+      Contract.Ensures(Contract.Result<string>().Length >= 4, @" length >= 4 since file name must end with '.TMP'");
       Contract.EnsuresOnThrow<System.IO.IOException>(true, @"An I/O error occurs, such as no unique temporary file name is available. - or - This method was unable to create a temporary file.");
       return default(string);
     }