diff options
| author | Vincent Laporte | 2018-10-04 09:57:09 +0000 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-10-09 18:17:40 +0200 |
| commit | 41dcd52864a569d2a0305ce97ad335238a0bc17d (patch) | |
| tree | b30a14ff4cae80ba175f03be7da204d0635e2129 | |
| parent | e739af593ae0a9ca20a839aa2a481628dd768ef6 (diff) | |
[default.nix] Add install dir to OCAMLPATH before running the test-suite
| -rw-r--r-- | default.nix | 1 | ||||
| -rw-r--r-- | test-suite/Makefile | 5 |
2 files changed, 5 insertions, 1 deletions
diff --git a/default.nix b/default.nix index a5c4c1fbb9..1cc74dc0d2 100644 --- a/default.nix +++ b/default.nix @@ -93,6 +93,7 @@ stdenv.mkDerivation rec { preInstallCheck = '' patchShebangs tools/ patchShebangs test-suite/ + export OCAMLPATH=$OCAMLFIND_DESTDIR:$OCAMLPATH ''; installCheckTarget = [ "check" ]; diff --git a/test-suite/Makefile b/test-suite/Makefile index 5e465ab47d..d088702b44 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -250,8 +250,11 @@ $(addsuffix .log,$(wildcard bugs/closed/*.v)): %.v.log: %.v # Unit tests ####################################################################### +# COQLIBINSTALL is quoted in config/make thus we must unquote it, +# otherwise the directory name will include the quotes, see +# see for example https://stackoverflow.com/questions/10424645/how-to-convert-a-quoted-string-to-a-normal-one-in-makefile ifeq ($(LOCAL),true) - export OCAMLPATH := $(patsubst "%",%,$(COQLIBINSTALL)) + export OCAMLPATH := $(shell echo $(COQLIBINSTALL)) endif OCAMLOPT := $(OCAMLFIND) opt $(CAMLFLAGS) |