diff options
| author | Maxime Dénès | 2017-06-02 16:18:31 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-06-02 16:18:31 +0200 |
| commit | c1d1dde20093531017889d57be837c5e2e4ecb9c (patch) | |
| tree | 67c9acb7f5874f86c5fdffd63fbad6facfa5264f | |
| parent | 13e8983e3be6bff993c212d7fdcf707cf3c749c6 (diff) | |
| parent | b4fd775380694f62fc89bec459f1e96723da4283 (diff) | |
Merge PR#691: [travis] Add OSX test-suite checking.
| -rw-r--r-- | .travis.yml | 13 | ||||
| -rw-r--r-- | test-suite/.csdp.cache | bin | 89077 -> 89077 bytes | |||
| -rwxr-xr-x | test-suite/coq-makefile/native1/run.sh | 3 | ||||
| -rw-r--r-- | tools/CoqMakefile.in | 5 |
4 files changed, 16 insertions, 5 deletions
diff --git a/.travis.yml b/.travis.yml index 14bafd3456..e794981245 100644 --- a/.travis.yml +++ b/.travis.yml @@ -31,6 +31,7 @@ env: # system is == 4.02.3 - COMPILER="system" - CAMLP5_VER="6.14" + - NATIVE_COMP="yes" # Main test suites matrix: - TEST_TARGET="test-suite" COMPILER="4.02.3+32bit" @@ -133,6 +134,16 @@ matrix: - avsm packages: *coqide-packages + - os: osx + env: + - TEST_TARGET="test-suite" + - COMPILER="system" + - CAMLP5_VER="6.17" + - NATIVE_COMP="no" + before_install: + - brew update + - brew install opam + install: - opam init -j ${NJOBS} --compiler=${COMPILER} -n -y - eval $(opam config env) @@ -144,7 +155,7 @@ script: - set -e - echo 'Configuring Coq...' && echo -en 'travis_fold:start:coq.config\\r' -- ./configure -local -usecamlp5 -native-compiler yes ${EXTRA_CONF} +- ./configure -local -usecamlp5 -native-compiler ${NATIVE_COMP} ${EXTRA_CONF} - echo -en 'travis_fold:end:coq.config\\r' - echo 'Building Coq...' && echo -en 'travis_fold:start:coq.build\\r' diff --git a/test-suite/.csdp.cache b/test-suite/.csdp.cache Binary files differindex ba85286dd3..b99d80e95f 100644 --- a/test-suite/.csdp.cache +++ b/test-suite/.csdp.cache diff --git a/test-suite/coq-makefile/native1/run.sh b/test-suite/coq-makefile/native1/run.sh index bc9f846dda..f079662631 100755 --- a/test-suite/coq-makefile/native1/run.sh +++ b/test-suite/coq-makefile/native1/run.sh @@ -3,7 +3,8 @@ #set -x set -e -if which ocamlopt; then +NATIVECOMP=`grep "let no_native_compiler = false" ../../../config/coq_config.ml`||true +if [[ `which ocamlopt` && $NATIVECOMP ]]; then . ../template/init.sh diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index fb064c495f..1308e91759 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -375,7 +375,7 @@ uninstall:: instf="$(DESTDIR)$(COQLIBINSTALL)/$$df/`basename $$f`"; \ rm -f "$$instf";\ echo RM "$$instf"; \ - rmdir --ignore-fail-on-non-empty "$(DESTDIR)$(COQLIBINSTALL)/$$df/"; \ + rmdir "$(DESTDIR)$(COQLIBINSTALL)/$$df/" || true; \ done .PHONY: uninstall @@ -385,8 +385,7 @@ uninstall-doc:: $(HIDE)rm -rf "$(DESTDIR)$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/html" $(SHOW)'RM $(DESTDIR)$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/mlihtml' $(HIDE)rm -rf "$(DESTDIR)$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/mlihtml" - $(HIDE)rmdir --ignore-fail-on-non-empty \ - "$(DESTDIR)$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/" + $(HIDE) rmdir "$(DESTDIR)$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/" || true .PHONY: uninstall-doc # Cleaning #################################################################### |