From e47c30bf431f3c8160b41384eedb538ba16578d0 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Fri, 29 May 2015 15:41:15 +0200
Subject: Flag -test-mode intended to be used for ad-hoc prints in test-suite

Of course there is an exception to the previous commit.
Fail used to print even if silenced but loading a vernac file.

This behavior is useful only in tests, hence this flag.
---
 test-suite/Makefile | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'test-suite')

diff --git a/test-suite/Makefile b/test-suite/Makefile
index cffbe48196..476d850ac9 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -30,7 +30,7 @@
 BIN := ../bin/
 LIB := ..
 
-coqtop := $(BIN)coqtop -boot -q -batch -R prerequisite TestSuite
+coqtop := $(BIN)coqtop -boot -q -batch -test-mode -R prerequisite TestSuite
 bincoqc := $(BIN)coqc -coqlib $(LIB) -R prerequisite TestSuite
 bincoqchk := $(BIN)coqchk -coqlib $(LIB) -R prerequisite TestSuite
 
-- 
cgit v1.2.3