diff options
| author | Ralf Treinen | 2020-03-10 21:33:16 +0100 |
|---|---|---|
| committer | Ralf Treinen | 2020-03-10 21:33:35 +0100 |
| commit | 47862b094536cd9120fbad06c4733c95716c314d (patch) | |
| tree | 446d10ac35252cd421be6183d9c6cd9fb0119157 /test-suite/coq-makefile | |
| parent | 3a5469b2097c55ecf952ead470caf03b6112cd9e (diff) | |
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.
Diffstat (limited to 'test-suite/coq-makefile')
| -rwxr-xr-x | test-suite/coq-makefile/camldep/run.sh | 8 |
1 files 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 ] |