aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--Makefile2
-rwxr-xr-xtest-suite/check6
2 files changed, 6 insertions, 2 deletions
diff --git a/Makefile b/Makefile
index 7803f8259f..9ac970c564 100644
--- a/Makefile
+++ b/Makefile
@@ -325,7 +325,7 @@ clean::
###########################################################################
check: $(BESTCOQTOP)
- cd test-suite; ./check
+ cd test-suite; ./check -$(BEST)
###########################################################################
# theories and states
diff --git a/test-suite/check b/test-suite/check
index f206c8413a..3e8a080384 100755
--- a/test-suite/check
+++ b/test-suite/check
@@ -2,7 +2,11 @@
# Automatic test of Coq
-command="../bin/coqtop.opt -q -batch -load-vernac-source"
+if [ "$1" = -byte ]; then
+ command="../bin/coqtop.byte -q -batch -load-vernac-source"
+else
+ command="../bin/coqtop -q -batch -load-vernac-source"
+fi
# on compte le nombre de tests et de succès
nbtests=0