aboutsummaryrefslogtreecommitdiffhomepage
path: root/.circleci
diff options
context:
space:
mode:
authorGravatar Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>2017-12-13 13:26:59 +0100
committerGravatar Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>2017-12-13 13:26:59 +0100
commitc2b7b15526f0c8b87b9442567ddfa0e133cfebcf (patch)
tree6d2d7d4ece83f9c0d98198249c5eb2a9d121e74e /.circleci
parent8323ac57d63d3734c5f43b787c97644bf2fce32d (diff)
Circle CI: enable native compiler.
Diffstat (limited to '.circleci')
-rw-r--r--.circleci/config.yml7
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