diff options
author | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-12-13 13:26:59 +0100 |
---|---|---|
committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-12-13 13:26:59 +0100 |
commit | c2b7b15526f0c8b87b9442567ddfa0e133cfebcf (patch) | |
tree | 6d2d7d4ece83f9c0d98198249c5eb2a9d121e74e /.circleci | |
parent | 8323ac57d63d3734c5f43b787c97644bf2fce32d (diff) |
Circle CI: enable native compiler.
Diffstat (limited to '.circleci')
-rw-r--r-- | .circleci/config.yml | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/.circleci/config.yml b/.circleci/config.yml index 42df67e71..fecabd7bc 100644 --- a/.circleci/config.yml +++ b/.circleci/config.yml @@ -13,6 +13,7 @@ defaults: NJOBS: 2 COMPILER: "system" CAMLP5_VER: "6.14" + NATIVE_COMP: "yes" # some useful values COMPILER_32BIT: &compiler-32bit "4.02.3+32bit" @@ -70,7 +71,7 @@ before_script: &before_script source ~/.profile echo 'start:coq.config' - ./configure -local -native-compiler no ${EXTRA_CONF} + ./configure -local -native-compiler ${NATIVE_COMP} ${EXTRA_CONF} echo 'end:coq.config' - run: &build-build name: Build @@ -151,7 +152,7 @@ before_script: &before_script name: Configure command: | source ~/.profile - ./configure -local ${EXTRA_CONF} + ./configure -local -native-compiler ${NATIVE_COMP} ${EXTRA_CONF} - run: name: Build @@ -160,7 +161,7 @@ before_script: &before_script make -j ${NJOBS} coqocaml environment: &warnings-variables <<: *envvars - EXTRA_CONF: "-native-compiler yes -coqide byte -byte-only" + EXTRA_CONF: "-coqide byte -byte-only" EXTRA_PACKAGES: *coqide-packages EXTRA_OPAM: *coqide-opam |