Merge PR #897: Fix test suite on windows (wrt fake_ide and coq-makefile)

21 files changed, 34 insertions, 65 deletions

diff --git a/test-suite/coq-makefile/arg/run.sh b/test-suite/coq-makefile/arg/run.sh
index e98da17c78..e7de90ff2f 100755
--- a/test-suite/coq-makefile/arg/run.sh
+++ b/test-suite/coq-makefile/arg/run.sh
@@ -1,9 +1,7 @@
 #!/usr/bin/env bash
 
-#set -x
-set -e
-
 . ../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 28d9878f9b..221dcd7bf8 100755
--- a/test-suite/coq-makefile/compat-subdirs/run.sh
+++ b/test-suite/coq-makefile/compat-subdirs/run.sh
@@ -1,9 +1,8 @@
 #!/usr/bin/env bash
 
-#set -x
-set -e
-
 . ../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 e8291c89da..1feff7479b 100755
--- a/test-suite/coq-makefile/coqdoc1/run.sh
+++ b/test-suite/coq-makefile/coqdoc1/run.sh
@@ -1,17 +1,15 @@
 #!/usr/bin/env bash
 
-#set -x
-set -e
-
 . ../template/init.sh
 
 coq_makefile -f _CoqProject -o Makefile
+cat Makefile.conf
 make
 make html mlihtml
 make install DSTROOT="$PWD/tmp"
 make install-doc DSTROOT="$PWD/tmp"
 #make debug
-(for d in `find tmp -name user-contrib`; do pushd $d >/dev/null; find .; popd >/dev/null; done) | sort -u > actual
+(for d in `find tmp -name user-contrib` ; do pushd $d >/dev/null && find . && popd >/dev/null; done) | sort -u > actual
 sort -u > desired <<EOT
 .
 ./test
diff --git a/test-suite/coq-makefile/coqdoc2/run.sh b/test-suite/coq-makefile/coqdoc2/run.sh
index e8291c89da..1feff7479b 100755
--- a/test-suite/coq-makefile/coqdoc2/run.sh
+++ b/test-suite/coq-makefile/coqdoc2/run.sh
@@ -1,17 +1,15 @@
 #!/usr/bin/env bash
 
-#set -x
-set -e
-
 . ../template/init.sh
 
 coq_makefile -f _CoqProject -o Makefile
+cat Makefile.conf
 make
 make html mlihtml
 make install DSTROOT="$PWD/tmp"
 make install-doc DSTROOT="$PWD/tmp"
 #make debug
-(for d in `find tmp -name user-contrib`; do pushd $d >/dev/null; find .; popd >/dev/null; done) | sort -u > actual
+(for d in `find tmp -name user-contrib` ; do pushd $d >/dev/null && find . && popd >/dev/null; done) | sort -u > actual
 sort -u > desired <<EOT
 .
 ./test
diff --git a/test-suite/coq-makefile/extend-subdirs/run.sh b/test-suite/coq-makefile/extend-subdirs/run.sh
index ea5792a937..221dcd7bf8 100755
--- a/test-suite/coq-makefile/extend-subdirs/run.sh
+++ b/test-suite/coq-makefile/extend-subdirs/run.sh
@@ -1,10 +1,8 @@
 #!/usr/bin/env bash
 
-#set -x
-set -e
-
 . ../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 214a9d5b28..b2c5d5669b 100755
--- a/test-suite/coq-makefile/latex1/run.sh
+++ b/test-suite/coq-makefile/latex1/run.sh
@@ -1,13 +1,11 @@
 #!/usr/bin/env bash
 
-#set -x
-set -e
-
 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 752c0c2cea..1f262a9390 100755
--- a/test-suite/coq-makefile/merlin1/run.sh
+++ b/test-suite/coq-makefile/merlin1/run.sh
@@ -1,11 +1,9 @@
 #!/usr/bin/env bash
 
-#set -x
-set -e
-
 . ../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 10a200ddee..51669f28f5 100755
--- a/test-suite/coq-makefile/mlpack1/run.sh
+++ b/test-suite/coq-makefile/mlpack1/run.sh
@@ -1,16 +1,14 @@
 #!/usr/bin/env bash
 
-#set -x
-set -e
-
 . ../template/init.sh
 
 coq_makefile -f _CoqProject -o Makefile
+cat Makefile.conf
 make
 make html mlihtml
 make install DSTROOT="$PWD/tmp"
 #make debug
-(cd `find tmp -name user-contrib`; find .) | sort > actual
+(cd `find tmp -name user-contrib` && find .) | sort > actual
 sort > desired <<EOT
 .
 ./test
diff --git a/test-suite/coq-makefile/mlpack2/run.sh b/test-suite/coq-makefile/mlpack2/run.sh
index 10a200ddee..51669f28f5 100755
--- a/test-suite/coq-makefile/mlpack2/run.sh
+++ b/test-suite/coq-makefile/mlpack2/run.sh
@@ -1,16 +1,14 @@
 #!/usr/bin/env bash
 
-#set -x
-set -e
-
 . ../template/init.sh
 
 coq_makefile -f _CoqProject -o Makefile
+cat Makefile.conf
 make
 make html mlihtml
 make install DSTROOT="$PWD/tmp"
 #make debug
-(cd `find tmp -name user-contrib`; find .) | sort > actual
+(cd `find tmp -name user-contrib` && find .) | sort > actual
 sort > desired <<EOT
 .
 ./test
diff --git a/test-suite/coq-makefile/multiroot/run.sh b/test-suite/coq-makefile/multiroot/run.sh
index 3cd1ac305f..d3bb53106d 100755
--- a/test-suite/coq-makefile/multiroot/run.sh
+++ b/test-suite/coq-makefile/multiroot/run.sh
@@ -1,19 +1,17 @@
 #!/usr/bin/env bash
 
-#set -x
-set -e
-
 . ../template/init.sh
 
 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"
 make install-doc DSTROOT="$PWD/tmp"
 #make debug
-(for d in `find tmp -name user-contrib`; do pushd $d >/dev/null; find .; popd >/dev/null; done) | sort -u > actual
+(for d in `find tmp -name user-contrib` ; do pushd $d >/dev/null && find . && popd >/dev/null; done) | sort -u > actual
 sort > desired <<EOT
 .
 ./test
diff --git a/test-suite/coq-makefile/native1/run.sh b/test-suite/coq-makefile/native1/run.sh
index 9f6295d644..3bec11cb75 100755
--- a/test-suite/coq-makefile/native1/run.sh
+++ b/test-suite/coq-makefile/native1/run.sh
@@ -1,19 +1,17 @@
 #!/usr/bin/env bash
 
-#set -x
-set -e
-
 NATIVECOMP=`grep "let no_native_compiler = false" ../../../config/coq_config.ml`||true
 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"
 #make debug
-(cd `find tmp -name user-contrib`; find .) | sort > actual
+(cd `find tmp -name user-contrib` && find .) | sort > actual
 sort > desired <<EOT
 .
 ./test
diff --git a/test-suite/coq-makefile/only/run.sh b/test-suite/coq-makefile/only/run.sh
index 2ea3deffb7..8cf04bf2cd 100755
--- a/test-suite/coq-makefile/only/run.sh
+++ b/test-suite/coq-makefile/only/run.sh
@@ -1,11 +1,9 @@
 #!/usr/bin/env bash
 
-#set -x
-set -e
-
 . ../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 c2d47166fe..5433d9e92d 100755
--- a/test-suite/coq-makefile/plugin1/run.sh
+++ b/test-suite/coq-makefile/plugin1/run.sh
@@ -1,17 +1,15 @@
 #!/usr/bin/env bash
 
-#set -x
-set -e
-
 . ../template/init.sh
 
 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"
 #make debug
-(cd `find tmp -name user-contrib`; find .) | sort > actual
+(cd `find tmp -name user-contrib` && find .) | sort > actual
 sort > desired <<EOT
 .
 ./test
diff --git a/test-suite/coq-makefile/plugin2/run.sh b/test-suite/coq-makefile/plugin2/run.sh
index c2d47166fe..5433d9e92d 100755
--- a/test-suite/coq-makefile/plugin2/run.sh
+++ b/test-suite/coq-makefile/plugin2/run.sh
@@ -1,17 +1,15 @@
 #!/usr/bin/env bash
 
-#set -x
-set -e
-
 . ../template/init.sh
 
 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"
 #make debug
-(cd `find tmp -name user-contrib`; find .) | sort > actual
+(cd `find tmp -name user-contrib` && find .) | sort > actual
 sort > desired <<EOT
 .
 ./test
diff --git a/test-suite/coq-makefile/plugin3/run.sh b/test-suite/coq-makefile/plugin3/run.sh
index c2d47166fe..5433d9e92d 100755
--- a/test-suite/coq-makefile/plugin3/run.sh
+++ b/test-suite/coq-makefile/plugin3/run.sh
@@ -1,17 +1,15 @@
 #!/usr/bin/env bash
 
-#set -x
-set -e
-
 . ../template/init.sh
 
 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"
 #make debug
-(cd `find tmp -name user-contrib`; find .) | sort > actual
+(cd `find tmp -name user-contrib` && find .) | sort > actual
 sort > desired <<EOT
 .
 ./test
diff --git a/test-suite/coq-makefile/template/init.sh b/test-suite/coq-makefile/template/init.sh
index c952d41a30..803fe8029a 100755
--- a/test-suite/coq-makefile/template/init.sh
+++ b/test-suite/coq-makefile/template/init.sh
@@ -1,3 +1,5 @@
+set -e
+set -o pipefail
 
 export PATH=$COQBIN:$PATH
 
diff --git a/test-suite/coq-makefile/uninstall1/run.sh b/test-suite/coq-makefile/uninstall1/run.sh
index e525e12086..5354f794f7 100755
--- a/test-suite/coq-makefile/uninstall1/run.sh
+++ b/test-suite/coq-makefile/uninstall1/run.sh
@@ -1,11 +1,9 @@
 #!/usr/bin/env bash
 
-#set -x
-set -e
-
 . ../template/init.sh
 
 coq_makefile -f _CoqProject -o Makefile
+cat Makefile.conf
 make
 make html mlihtml
 make install DSTROOT="$PWD/tmp"
@@ -13,7 +11,7 @@ make install-doc DSTROOT="$PWD/tmp"
 make uninstall DSTROOT="$PWD/tmp"
 make uninstall-doc DSTROOT="$PWD/tmp"
 #make debug
-(for d in `find tmp -name user-contrib`; do pushd $d >/dev/null; find .; popd >/dev/null; done) | sort -u > actual
+(for d in `find tmp -name user-contrib` ; do pushd $d >/dev/null && find . && popd >/dev/null; done) | sort -u > actual
 sort -u > desired <<EOT
 .
 EOT
diff --git a/test-suite/coq-makefile/uninstall2/run.sh b/test-suite/coq-makefile/uninstall2/run.sh
index e525e12086..5354f794f7 100755
--- a/test-suite/coq-makefile/uninstall2/run.sh
+++ b/test-suite/coq-makefile/uninstall2/run.sh
@@ -1,11 +1,9 @@
 #!/usr/bin/env bash
 
-#set -x
-set -e
-
 . ../template/init.sh
 
 coq_makefile -f _CoqProject -o Makefile
+cat Makefile.conf
 make
 make html mlihtml
 make install DSTROOT="$PWD/tmp"
@@ -13,7 +11,7 @@ make install-doc DSTROOT="$PWD/tmp"
 make uninstall DSTROOT="$PWD/tmp"
 make uninstall-doc DSTROOT="$PWD/tmp"
 #make debug
-(for d in `find tmp -name user-contrib`; do pushd $d >/dev/null; find .; popd >/dev/null; done) | sort -u > actual
+(for d in `find tmp -name user-contrib` ; do pushd $d >/dev/null && find . && popd >/dev/null; done) | sort -u > actual
 sort -u > desired <<EOT
 .
 EOT
diff --git a/test-suite/coq-makefile/validate1/run.sh b/test-suite/coq-makefile/validate1/run.sh
index aaa4194b38..43bf39de10 100755
--- a/test-suite/coq-makefile/validate1/run.sh
+++ b/test-suite/coq-makefile/validate1/run.sh
@@ -1,10 +1,8 @@
 #!/usr/bin/env bash
 
-#set -x
-set -e
-
 . ../template/init.sh
 
 coq_makefile -f _CoqProject -o Makefile
+cat Makefile.conf
 make
 exec make validate