aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorMaxime Dénès2017-09-05 15:58:01 +0200
committerMaxime Dénès2017-09-05 15:58:01 +0200
commitdf6ae3d59af8f880a0411217b8e6f0dae0b92133 (patch)
tree1a2ffc0588c5ca6afa08ea1b7d8adbe2a9b37fa7
parentbb5fa2a3a2a1e398683d38a8731faa2ff3ec39b0 (diff)
parentc2c1f7e74d13bf614a8704de1437d4c789b2c2c9 (diff)
Merge PR #1011: fix test-suite/coq-makefile/findlib-package on windows after #958
-rw-r--r--appveyor.yml3
-rw-r--r--test-suite/coq-makefile/findlib-package/findlib/foo/Makefile4
-rwxr-xr-xtest-suite/coq-makefile/findlib-package/run.sh5
3 files changed, 8 insertions, 4 deletions
diff --git a/appveyor.yml b/appveyor.yml
index 3b08584ff5..ea31075a65 100644
--- a/appveyor.yml
+++ b/appveyor.yml
@@ -22,5 +22,4 @@ build_script:
- cmd: '%CYGROOT%/bin/bash -lc "cd $APPVEYOR_BUILD_FOLDER && ./configure -local && make"'
test_script:
-- cmd: '%CYGROOT%/bin/bash -lc "cd $APPVEYOR_BUILD_FOLDER && make -C test-suite all
- INTERACTIVE= && make validate"'
+- cmd: '%CYGROOT%/bin/bash -lc "cd $APPVEYOR_BUILD_FOLDER && make byte && make -C test-suite all INTERACTIVE= && make validate"'
diff --git a/test-suite/coq-makefile/findlib-package/findlib/foo/Makefile b/test-suite/coq-makefile/findlib-package/findlib/foo/Makefile
index 31cf116652..1615bfd067 100644
--- a/test-suite/coq-makefile/findlib-package/findlib/foo/Makefile
+++ b/test-suite/coq-makefile/findlib-package/findlib/foo/Makefile
@@ -1,7 +1,7 @@
-include ../../Makefile.conf
-CO=$(COQMF_OCAMLFIND) opt
-CB=$(COQMF_OCAMLFIND) ocamlc
+CO="$(COQMF_OCAMLFIND)" opt
+CB="$(COQMF_OCAMLFIND)" ocamlc
all:
$(CO) -c foolib.ml
diff --git a/test-suite/coq-makefile/findlib-package/run.sh b/test-suite/coq-makefile/findlib-package/run.sh
index a0d8a7fea7..5b24df6397 100755
--- a/test-suite/coq-makefile/findlib-package/run.sh
+++ b/test-suite/coq-makefile/findlib-package/run.sh
@@ -4,6 +4,11 @@
echo "let () = Foolib.foo ();;" >> src/test_aux.ml
export OCAMLPATH=$OCAMLPATH:$PWD/findlib
+if which cygpath 2>/dev/null; then
+ # the only way I found to pass OCAMLPATH on win is to have it contain
+ # only one entry
+ export OCAMLPATH=`cygpath -w $PWD/findlib`
+fi
make -C findlib/foo clean
coq_makefile -f _CoqProject -o Makefile
cat Makefile.conf