aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/Makefile
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2014-09-16 16:57:59 +0200
committerGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2014-09-16 17:34:57 +0200
commit4dc8746cac24ba72a1ec4dfa764a1ae88ce79277 (patch)
tree2987141c16e3ec03afc1d3b11cb3d7b3334c6580 /test-suite/Makefile
parent26aa224293e88611dcb543e400488013bc8b30b4 (diff)
Undo prints only if coqtop || emacs
Diffstat (limited to 'test-suite/Makefile')
-rw-r--r--test-suite/Makefile2
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile
index 0f7abb78e..74e806138 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -33,7 +33,7 @@ LIB := ..
coqtop := $(BIN)coqtop -boot -q -batch -R prerequisite TestSuite
bincoqc := $(BIN)coqc -coqlib $(LIB) -R prerequisite TestSuite
-command := $(coqtop) -top Top -load-vernac-source
+command := $(coqtop) -top Top -async-proofs-cache force -load-vernac-source
coqc := $(coqtop) -compile
coqdep := $(BIN)coqdep -coqlib $(LIB)