aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/Makefile
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2017-05-31 22:59:21 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2017-05-31 22:59:21 +0200
commite732ef4d2e6e22eb39f5fc5af80124dfcbfdb950 (patch)
tree4efa7e900d67801e7fb99c3c53caf55e1f7f415b /test-suite/Makefile
parenteed90d1bd867dce59f6bf1b2bf769fff188f128b (diff)
parent2712ea67dad04faa52871564b79efd1c82127294 (diff)
Merge PR#701: [readlink -f] doesn't work on OSX
Diffstat (limited to 'test-suite/Makefile')
-rw-r--r--test-suite/Makefile2
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile
index 285460762..6c04abcaa 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
-BIN := $(shell cd ..; readlink -f bin)/
LIB := $(shell cd ..; pwd)
+BIN := $(LIB)/bin/
coqtop := $(BIN)coqtop -coqlib $(LIB) -boot -q -batch -test-mode -R prerequisite TestSuite
coqc := $(BIN)coqc -coqlib $(LIB) -R prerequisite TestSuite