From 91cee1c2028f9ad995df863f2a4568d95f4ea1a8 Mon Sep 17 00:00:00 2001 From: qunyanm Date: Mon, 28 Mar 2016 12:02:37 -0700 Subject: Make /autoTriggers:1 to be default. Add /autoTriggers:0 to tests that requires it. Don't use pretty warning signs since we can't diff them correctly in the test output from the test run. --- Test/cloudmake/CloudMake-ParallelBuilds.dfy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'Test/cloudmake/CloudMake-ParallelBuilds.dfy') diff --git a/Test/cloudmake/CloudMake-ParallelBuilds.dfy b/Test/cloudmake/CloudMake-ParallelBuilds.dfy index 07cae317..5cc70994 100644 --- a/Test/cloudmake/CloudMake-ParallelBuilds.dfy +++ b/Test/cloudmake/CloudMake-ParallelBuilds.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t" +// RUN: %dafny /compile:0 /dprint:"%t.dprint" /autoTriggers:0 "%s" > "%t" // RUN: %diff "%s.expect" "%t" // This module proves the correctness of the algorithms. It leaves a number of things undefined. -- cgit v1.2.3