aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rwxr-xr-xtest-suite/coq-makefile/findlib-package-unpacked/run.sh4
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