aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
diff options
context:
space:
mode:
authorGravatar pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-09-04 17:45:46 +0000
committerGravatar pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-09-04 17:45:46 +0000
commit6c3451cf2aef8b5dc9ee7833b050816f76bec10d (patch)
treebf2455b0bc589b54f7136d9c5254feb22d3920f8 /test-suite
parent74a7deb56575f6ed86208329570a19b75c08390d (diff)
test-suite uses coqtop instead of coqtop.byte
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15769 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite')
-rw-r--r--test-suite/Makefile2
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile
index 447160e59..0b75a01bb 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -30,7 +30,7 @@
BIN := ../bin/
LIB := ..
-coqtop := $(BIN)coqtop.byte -boot -q -batch -I prerequisite
+coqtop := $(BIN)coqtop -boot -q -batch -I prerequisite
bincoqc := $(BIN)coqc -coqlib $(LIB) -I prerequisite
command := $(coqtop) -top Top -load-vernac-source