aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2017-06-21 14:51:42 +0200
committerGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2017-07-20 15:40:48 +0200
commit9682fea9f71477af58681735d8829507991d27c5 (patch)
tree56a5b6647c990bc9c8b919f07cb5c91abd90b549 /test-suite
parent7af3bdf56f278e8928df7bdf63fddd159be610ec (diff)
Make coqlib relative in test suite (revert 024a7ab20b0)
Diffstat (limited to 'test-suite')
-rw-r--r--test-suite/Makefile4
1 files changed, 2 insertions, 2 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile
index 5ab4cacda..52127a45d 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -27,8 +27,8 @@
# Default value when called from a freshly compiled Coq, but can be
# easily overridden
-LIB := $(shell cd ..; pwd)
-BIN := $(LIB)/bin/
+LIB := ..
+BIN := $(shell cd ..; pwd)/bin/
coqtop := $(BIN)coqtop -coqlib $(LIB) -boot -q -batch -test-mode -R prerequisite TestSuite
coqc := $(BIN)coqc -coqlib $(LIB) -R prerequisite TestSuite