From 191ff327c49796e8a64fae893520d878b32d3268 Mon Sep 17 00:00:00 2001
From: Clément Pit--Claudel <clement.pitclaudel@live.com>
Date: Sun, 7 Jun 2015 12:38:31 -0700
Subject: Fix the UseBaseNameForFileName flag; it shouldn't set the return code
 to zero.

The test suite relies on error codes all being zero (except for preprocessing
errors), so add a flag for that (as suggested in a source comment).
---
 Source/DafnyDriver/DafnyDriver.cs | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'Source/DafnyDriver')

diff --git a/Source/DafnyDriver/DafnyDriver.cs b/Source/DafnyDriver/DafnyDriver.cs
index 854269c1..a769b829 100644
--- a/Source/DafnyDriver/DafnyDriver.cs
+++ b/Source/DafnyDriver/DafnyDriver.cs
@@ -104,9 +104,8 @@ namespace Microsoft.Dafny
           Console.WriteLine("Press Enter to exit.");
           Console.ReadLine();
         }
-        if (CommandLineOptions.Clo.UseBaseNameForFileName && exitValue != ExitValue.PREPROCESSING_ERROR)
+        if (!DafnyOptions.O.CountVerificationErrors && exitValue != ExitValue.PREPROCESSING_ERROR)
         {
-          // TODO(wuestholz): We should probably add a separate flag for this. This is currently only used by the new testing infrastructure.
           return 0;
         }
         //Console.ReadKey();
-- 
cgit v1.2.3