From 47862b094536cd9120fbad06c4733c95716c314d Mon Sep 17 00:00:00 2001
From: Ralf Treinen
Date: Tue, 10 Mar 2020 21:33:16 +0100
Subject: test coq-makefile/camldep: try to build a cmx only when there is an
 ocamlopt compiler. In any case, try to build a cmo file.

---
 test-suite/coq-makefile/camldep/run.sh | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

diff --git a/test-suite/coq-makefile/camldep/run.sh b/test-suite/coq-makefile/camldep/run.sh
index aa62ee56eb..465677a4bf 100755
--- a/test-suite/coq-makefile/camldep/run.sh
+++ b/test-suite/coq-makefile/camldep/run.sh
@@ -13,5 +13,9 @@ mkdir src
 echo '{ let foo = () }' > src/file1.mlg
 echo 'let bar = File1.foo' > src/file2.ml
 coq_makefile -f _CoqProject -o Makefile
-make src/file2.cmx
-[ -f src/file2.cmx ]
+if which ocamlopt >/dev/null 2>&1; then
+    make src/file2.cmx
+    [ -f src/file2.cmx ]
+fi
+make src/file2.cmo
+[ -f src/file2.cmo ]
-- 
cgit v1.2.3


From d22db7a4a3c95bbbe6a4d7a25ed08f9d99fa64e8 Mon Sep 17 00:00:00 2001
From: Ralf Treinen
Date: Tue, 10 Mar 2020 21:36:04 +0100
Subject: test coq-makefile/findlib-package-unpacked: only try to invoke 'make'
 when there is an ocamlopt compiler.

---
 test-suite/coq-makefile/findlib-package-unpacked/run.sh | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

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
-- 
cgit v1.2.3