diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-06-02 16:18:31 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-06-02 16:18:31 +0200 |
| commit | c1d1dde20093531017889d57be837c5e2e4ecb9c (patch) | |
| tree | 67c9acb7f5874f86c5fdffd63fbad6facfa5264f /test-suite | |
| parent | 13e8983e3be6bff993c212d7fdcf707cf3c749c6 (diff) | |
| parent | b4fd775380694f62fc89bec459f1e96723da4283 (diff) | |
Merge PR#691: [travis] Add OSX test-suite checking.
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/.csdp.cache | bin | 89077 -> 89077 bytes | |||
| -rwxr-xr-x | test-suite/coq-makefile/native1/run.sh | 3 |
2 files changed, 2 insertions, 1 deletions
diff --git a/test-suite/.csdp.cache b/test-suite/.csdp.cache Binary files differindex ba85286dd..b99d80e95 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 bc9f846dd..f07966263 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 |