aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorherbelin2005-12-18 10:31:40 +0000
committerherbelin2005-12-18 10:31:40 +0000
commit309772bf2177058fde2858aefb9d8e1b06936adf (patch)
tree215256a15d3bda20e861b991db7720d96da7cda2
parentf37179a09a0c4d64f247c955735d068a29c5998d (diff)
L'option -no-vm laisse la place à une option -vm
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7667 85f007b7-540e-0410-9357-904b9bb8a0f7
-rwxr-xr-xtest-suite/check8
1 files changed, 4 insertions, 4 deletions
diff --git a/test-suite/check b/test-suite/check
index d8f7960003..af5568399b 100755
--- a/test-suite/check
+++ b/test-suite/check
@@ -9,15 +9,15 @@ else
fi
if [ "$1" = -byte ]; then
- command="../bin/coqtop.byte -no-vm -q -batch -load-vernac-source"
+ command="../bin/coqtop.byte -q -batch -load-vernac-source"
else
- command="../bin/coqtop -no-vm -q -batch -load-vernac-source"
+ command="../bin/coqtop -q -batch -load-vernac-source"
fi
if [ "$1" = -byte ]; then
- coqtop="../bin/coqtop.byte -no-vm -q -batch"
+ coqtop="../bin/coqtop.byte -q -batch"
else
- coqtop="../bin/coqtop -no-vm -q -batch"
+ coqtop="../bin/coqtop -q -batch"
fi
# on compte le nombre de tests et de succès