summaryrefslogtreecommitdiff
path: root/test-suite/check
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2009-02-01 00:54:40 +0100
committerGravatar Stephane Glondu <steph@glondu.net>2009-02-01 00:54:40 +0100
commitcfbfe13f5b515ae2e3c6cdd97e2ccee03bc26e56 (patch)
treeb7832bd5d412a5a5d69cb36ae2ded62c71124c22 /test-suite/check
parent113b703a695acbe31ac6dd6a8c4aa94f6fda7545 (diff)
Imported Upstream version 8.2~rc2+dfsgupstream/8.2.rc2+dfsg
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"