summaryrefslogtreecommitdiff
path: root/test-suite/check
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/check')
-rwxr-xr-xtest-suite/check4
1 files changed, 2 insertions, 2 deletions
diff --git a/test-suite/check b/test-suite/check
index 47960e98..bed86c41 100755
--- a/test-suite/check
+++ b/test-suite/check
@@ -3,9 +3,9 @@
# Automatic test of Coq
if [ "$1" = -byte ]; then
- coqtop="../bin/coqtop.byte -q -batch"
+ coqtop="../bin/coqtop.byte -boot -q -batch"
else
- coqtop="../bin/coqtop -q -batch"
+ coqtop="../bin/coqtop -boot -q -batch"
fi
command="$coqtop -top Top -load-vernac-source"