diff options
| author | Gaëtan Gilbert | 2018-07-24 13:51:59 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-07-24 13:51:59 +0200 |
| commit | 388e65b550a6dd12fa4e59b26e03a831ebd842ce (patch) | |
| tree | 44d6931ed32bc21f50b8fa1dcde4fe725d84b72a | |
| parent | 4ab54f3cca76632cb6e258c84abc259e15e9e9f8 (diff) | |
| parent | 3cb3ca518b80763624fc643363cd4540ff299cc0 (diff) | |
Merge PR #8040: [ci] Enable native compiler in `egde:flambda` build.
| -rw-r--r-- | .gitlab-ci.yml | 2 | ||||
| -rw-r--r-- | .travis.yml | 3 |
2 files changed, 2 insertions, 3 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index be19a93a37..c2ca6ebaa4 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -200,7 +200,7 @@ build:edge+flambda: variables: OPAM_SWITCH: edge OPAM_VARIANT: "+flambda" - COQ_EXTRA_CONF: "-native-compiler no -coqide opt -flambda-opts " + COQ_EXTRA_CONF: "-native-compiler yes -coqide opt -flambda-opts " COQ_EXTRA_CONF_QUOTE: "-O3 -unbox-closures" windows64: diff --git a/.travis.yml b/.travis.yml index 53fbe5821a..f8b047ea18 100644 --- a/.travis.yml +++ b/.travis.yml @@ -65,7 +65,7 @@ matrix: - TEST_TARGET="validate" COMPILER="4.02.3+32bit" TW="travis_wait" - if: NOT (type = pull_request) env: - - TEST_TARGET="validate" COMPILER="${COMPILER_BE}+flambda" CAMLP5_VER="${CAMLP5_VER_BE}" NATIVE_COMP="no" EXTRA_CONF="-flambda-opts -O3" FINDLIB_VER="${FINDLIB_VER_BE}" + - TEST_TARGET="validate" COMPILER="${COMPILER_BE}+flambda" CAMLP5_VER="${CAMLP5_VER_BE}" EXTRA_CONF="-flambda-opts -O3" FINDLIB_VER="${FINDLIB_VER_BE}" - if: NOT (type = pull_request) env: - TEST_TARGET="ci-coq-dpdgraph" EXTRA_OPAM="ocamlgraph" @@ -154,7 +154,6 @@ matrix: - COMPILER="${COMPILER_BE}+flambda" - FINDLIB_VER="${FINDLIB_VER_BE}" - CAMLP5_VER="${CAMLP5_VER_BE}" - - NATIVE_COMP="no" - EXTRA_CONF="-coqide opt -with-doc yes -flambda-opts -O3" - EXTRA_OPAM="${LABLGTK_BE} ounit" before_install: *sphinx-install |