diff options
author | Gaëtan Gilbert <gaetan.gilbert@ens-lyon.fr> | 2017-05-30 15:25:45 +0200 |
---|---|---|
committer | Gaëtan Gilbert <gaetan.gilbert@ens-lyon.fr> | 2017-05-30 15:25:45 +0200 |
commit | 2712ea67dad04faa52871564b79efd1c82127294 (patch) | |
tree | 38c7b86542d14d54dce614c0744dd11e69f2282a /test-suite/Makefile | |
parent | fd36c0451c26e44b1b7e93299d3367ad2d35fee3 (diff) |
[readlink -f] doesn't work on OSX
We only want an absolute path, no need to follow symlinks.
Diffstat (limited to 'test-suite/Makefile')
-rw-r--r-- | test-suite/Makefile | 2 |
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 |