diff options
20 files changed, 20 insertions, 0 deletions
diff --git a/test-suite/coq-makefile/arg/run.sh b/test-suite/coq-makefile/arg/run.sh index aa0f50001a..e7de90ff2f 100755 --- a/test-suite/coq-makefile/arg/run.sh +++ b/test-suite/coq-makefile/arg/run.sh @@ -3,4 +3,5 @@ . ../template/init.sh coq_makefile -f _CoqProject -o Makefile +cat Makefile.conf make diff --git a/test-suite/coq-makefile/compat-subdirs/run.sh b/test-suite/coq-makefile/compat-subdirs/run.sh index 211f73adc7..221dcd7bf8 100755 --- a/test-suite/coq-makefile/compat-subdirs/run.sh +++ b/test-suite/coq-makefile/compat-subdirs/run.sh @@ -3,5 +3,6 @@ . ../template/init.sh coq_makefile -f _CoqProject -o Makefile +cat Makefile.conf make exec test -f "subdir/done" diff --git a/test-suite/coq-makefile/coqdoc1/run.sh b/test-suite/coq-makefile/coqdoc1/run.sh index 78e30bd354..1feff7479b 100755 --- a/test-suite/coq-makefile/coqdoc1/run.sh +++ b/test-suite/coq-makefile/coqdoc1/run.sh @@ -3,6 +3,7 @@ . ../template/init.sh coq_makefile -f _CoqProject -o Makefile +cat Makefile.conf make make html mlihtml make install DSTROOT="$PWD/tmp" diff --git a/test-suite/coq-makefile/coqdoc2/run.sh b/test-suite/coq-makefile/coqdoc2/run.sh index 78e30bd354..1feff7479b 100755 --- a/test-suite/coq-makefile/coqdoc2/run.sh +++ b/test-suite/coq-makefile/coqdoc2/run.sh @@ -3,6 +3,7 @@ . ../template/init.sh coq_makefile -f _CoqProject -o Makefile +cat Makefile.conf make make html mlihtml make install DSTROOT="$PWD/tmp" diff --git a/test-suite/coq-makefile/extend-subdirs/run.sh b/test-suite/coq-makefile/extend-subdirs/run.sh index 211f73adc7..221dcd7bf8 100755 --- a/test-suite/coq-makefile/extend-subdirs/run.sh +++ b/test-suite/coq-makefile/extend-subdirs/run.sh @@ -3,5 +3,6 @@ . ../template/init.sh coq_makefile -f _CoqProject -o Makefile +cat Makefile.conf make exec test -f "subdir/done" diff --git a/test-suite/coq-makefile/latex1/run.sh b/test-suite/coq-makefile/latex1/run.sh index 5337ca2952..b2c5d5669b 100755 --- a/test-suite/coq-makefile/latex1/run.sh +++ b/test-suite/coq-makefile/latex1/run.sh @@ -5,6 +5,7 @@ if which pdflatex; then . ../template/init.sh coq_makefile -f _CoqProject -o Makefile +cat Makefile.conf make exec make all.pdf diff --git a/test-suite/coq-makefile/merlin1/run.sh b/test-suite/coq-makefile/merlin1/run.sh index 37c5ab5c40..1f262a9390 100755 --- a/test-suite/coq-makefile/merlin1/run.sh +++ b/test-suite/coq-makefile/merlin1/run.sh @@ -3,6 +3,7 @@ . ../template/init.sh coq_makefile -f _CoqProject -o Makefile +cat Makefile.conf make .merlin cat > desired <<EOT B src diff --git a/test-suite/coq-makefile/mlpack1/run.sh b/test-suite/coq-makefile/mlpack1/run.sh index 1ca69bf230..51669f28f5 100755 --- a/test-suite/coq-makefile/mlpack1/run.sh +++ b/test-suite/coq-makefile/mlpack1/run.sh @@ -3,6 +3,7 @@ . ../template/init.sh coq_makefile -f _CoqProject -o Makefile +cat Makefile.conf make make html mlihtml make install DSTROOT="$PWD/tmp" diff --git a/test-suite/coq-makefile/mlpack2/run.sh b/test-suite/coq-makefile/mlpack2/run.sh index 1ca69bf230..51669f28f5 100755 --- a/test-suite/coq-makefile/mlpack2/run.sh +++ b/test-suite/coq-makefile/mlpack2/run.sh @@ -3,6 +3,7 @@ . ../template/init.sh coq_makefile -f _CoqProject -o Makefile +cat Makefile.conf make make html mlihtml make install DSTROOT="$PWD/tmp" diff --git a/test-suite/coq-makefile/multiroot/run.sh b/test-suite/coq-makefile/multiroot/run.sh index f23cf01495..d3bb53106d 100755 --- a/test-suite/coq-makefile/multiroot/run.sh +++ b/test-suite/coq-makefile/multiroot/run.sh @@ -5,6 +5,7 @@ cp -r theories theories2 mv src/test_plugin.mlpack src/test_plugin.mllib coq_makefile -f _CoqProject -o Makefile +cat Makefile.conf make make html mlihtml make install DSTROOT="$PWD/tmp" diff --git a/test-suite/coq-makefile/native1/run.sh b/test-suite/coq-makefile/native1/run.sh index 5a7b7694cc..3bec11cb75 100755 --- a/test-suite/coq-makefile/native1/run.sh +++ b/test-suite/coq-makefile/native1/run.sh @@ -6,6 +6,7 @@ if [[ `which ocamlopt` && $NATIVECOMP ]]; then . ../template/init.sh coq_makefile -f _CoqProject -o Makefile +cat Makefile.conf make make html mlihtml make install DSTROOT="$PWD/tmp" diff --git a/test-suite/coq-makefile/only/run.sh b/test-suite/coq-makefile/only/run.sh index 859a4bd7ea..8cf04bf2cd 100755 --- a/test-suite/coq-makefile/only/run.sh +++ b/test-suite/coq-makefile/only/run.sh @@ -3,6 +3,7 @@ . ../template/init.sh coq_makefile -f _CoqProject -o Makefile +cat Makefile.conf make only TGTS="src/test.cmi src/test_aux.cmi" -j2 test -f src/test.cmi test -f src/test_aux.cmi diff --git a/test-suite/coq-makefile/plugin-reach-outside-API-and-fail/run.sh b/test-suite/coq-makefile/plugin-reach-outside-API-and-fail/run.sh index 6301aa03c0..88606cd473 100755 --- a/test-suite/coq-makefile/plugin-reach-outside-API-and-fail/run.sh +++ b/test-suite/coq-makefile/plugin-reach-outside-API-and-fail/run.sh @@ -27,6 +27,7 @@ let _ = Pre_env.empty_env EOT ${COQBIN}coq_makefile -f _CoqProject -o Makefile +cat Makefile.conf if make VERBOSE=1; then # make command should have failed (but didn't) diff --git a/test-suite/coq-makefile/plugin-reach-outside-API-and-succeed-by-bypassing-the-API/run.sh b/test-suite/coq-makefile/plugin-reach-outside-API-and-succeed-by-bypassing-the-API/run.sh index 991fb4a61d..939ef9c7b7 100755 --- a/test-suite/coq-makefile/plugin-reach-outside-API-and-succeed-by-bypassing-the-API/run.sh +++ b/test-suite/coq-makefile/plugin-reach-outside-API-and-succeed-by-bypassing-the-API/run.sh @@ -28,5 +28,6 @@ let _ = Pre_env.empty_env EOT ${COQBIN}coq_makefile -f _CoqProject -o Makefile +cat Makefile.conf make VERBOSE=1 diff --git a/test-suite/coq-makefile/plugin1/run.sh b/test-suite/coq-makefile/plugin1/run.sh index abe715542d..5433d9e92d 100755 --- a/test-suite/coq-makefile/plugin1/run.sh +++ b/test-suite/coq-makefile/plugin1/run.sh @@ -4,6 +4,7 @@ mv src/test_plugin.mlpack src/test_plugin.mllib coq_makefile -f _CoqProject -o Makefile +cat Makefile.conf make make html mlihtml make install DSTROOT="$PWD/tmp" diff --git a/test-suite/coq-makefile/plugin2/run.sh b/test-suite/coq-makefile/plugin2/run.sh index abe715542d..5433d9e92d 100755 --- a/test-suite/coq-makefile/plugin2/run.sh +++ b/test-suite/coq-makefile/plugin2/run.sh @@ -4,6 +4,7 @@ mv src/test_plugin.mlpack src/test_plugin.mllib coq_makefile -f _CoqProject -o Makefile +cat Makefile.conf make make html mlihtml make install DSTROOT="$PWD/tmp" diff --git a/test-suite/coq-makefile/plugin3/run.sh b/test-suite/coq-makefile/plugin3/run.sh index abe715542d..5433d9e92d 100755 --- a/test-suite/coq-makefile/plugin3/run.sh +++ b/test-suite/coq-makefile/plugin3/run.sh @@ -4,6 +4,7 @@ mv src/test_plugin.mlpack src/test_plugin.mllib coq_makefile -f _CoqProject -o Makefile +cat Makefile.conf make make html mlihtml make install DSTROOT="$PWD/tmp" diff --git a/test-suite/coq-makefile/uninstall1/run.sh b/test-suite/coq-makefile/uninstall1/run.sh index ef90f99934..5354f794f7 100755 --- a/test-suite/coq-makefile/uninstall1/run.sh +++ b/test-suite/coq-makefile/uninstall1/run.sh @@ -3,6 +3,7 @@ . ../template/init.sh coq_makefile -f _CoqProject -o Makefile +cat Makefile.conf make make html mlihtml make install DSTROOT="$PWD/tmp" diff --git a/test-suite/coq-makefile/uninstall2/run.sh b/test-suite/coq-makefile/uninstall2/run.sh index ef90f99934..5354f794f7 100755 --- a/test-suite/coq-makefile/uninstall2/run.sh +++ b/test-suite/coq-makefile/uninstall2/run.sh @@ -3,6 +3,7 @@ . ../template/init.sh coq_makefile -f _CoqProject -o Makefile +cat Makefile.conf make make html mlihtml make install DSTROOT="$PWD/tmp" diff --git a/test-suite/coq-makefile/validate1/run.sh b/test-suite/coq-makefile/validate1/run.sh index 109acab85a..43bf39de10 100755 --- a/test-suite/coq-makefile/validate1/run.sh +++ b/test-suite/coq-makefile/validate1/run.sh @@ -3,5 +3,6 @@ . ../template/init.sh coq_makefile -f _CoqProject -o Makefile +cat Makefile.conf make exec make validate |