diff options
| author | Ralf Treinen | 2020-03-10 21:36:04 +0100 |
|---|---|---|
| committer | Ralf Treinen | 2020-03-10 21:36:09 +0100 |
| commit | d22db7a4a3c95bbbe6a4d7a25ed08f9d99fa64e8 (patch) | |
| tree | 3c1fcade0a77b4b36c477982bf98119d519fed61 /test-suite/coq-makefile | |
| parent | 47862b094536cd9120fbad06c4733c95716c314d (diff) | |
test coq-makefile/findlib-package-unpacked: only try to invoke 'make' when
there is an ocamlopt compiler.
Diffstat (limited to 'test-suite/coq-makefile')
| -rwxr-xr-x | test-suite/coq-makefile/findlib-package-unpacked/run.sh | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/test-suite/coq-makefile/findlib-package-unpacked/run.sh b/test-suite/coq-makefile/findlib-package-unpacked/run.sh index e53a7ed0f7..6d7ae15ee2 100755 --- a/test-suite/coq-makefile/findlib-package-unpacked/run.sh +++ b/test-suite/coq-makefile/findlib-package-unpacked/run.sh @@ -16,5 +16,7 @@ coq_makefile -f _CoqProject -o Makefile cat Makefile.conf cat Makefile.local make -C findlib/foo -make +if which ocamlopt >/dev/null 2>&1; then + make +fi make byte |