aboutsummaryrefslogtreecommitdiff
path: root/dev/ci/ci-compcert.sh
diff options
context:
space:
mode:
authorThéo Zimmermann2017-03-07 23:30:29 +0100
committerThéo Zimmermann2017-03-10 23:18:33 +0100
commit710c1e1f49ce834acb9488704bcbbf13c4ebaf91 (patch)
treed088d5a61426c8febb702866426c96a47a025b2b /dev/ci/ci-compcert.sh
parentba36aab9ad9a3d210211e1d4527dd0f6f493ca05 (diff)
[travis] Adding a template file and using it for all targets.
Diffstat (limited to 'dev/ci/ci-compcert.sh')
-rwxr-xr-xdev/ci/ci-compcert.sh5
1 files changed, 3 insertions, 2 deletions
diff --git a/dev/ci/ci-compcert.sh b/dev/ci/ci-compcert.sh
index 3b897f679a..111222ac7f 100755
--- a/dev/ci/ci-compcert.sh
+++ b/dev/ci/ci-compcert.sh
@@ -5,9 +5,10 @@ source ${ci_dir}/ci-common.sh
CompCert_CI_BRANCH=master
CompCert_CI_GITURL=https://github.com/AbsInt/CompCert.git
+CompCert_CI_DIR=${CI_BUILD_DIR}/CompCert
opam install -j ${NJOBS} -y menhir
-git_checkout ${CompCert_CI_BRANCH} ${CompCert_CI_GITURL} CompCert
+git_checkout ${CompCert_CI_BRANCH} ${CompCert_CI_GITURL} ${CompCert_CI_DIR}
# Patch to avoid the upper version limit
-( cd CompCert && sed -i.bak 's/8.6)/8.6|trunk)/' configure && ./configure x86_32-linux && make -j ${NJOBS} )
+( cd ${CompCert_CI_DIR} && sed -i.bak 's/8.6)/8.6|trunk)/' configure && ./configure x86_32-linux && make -j ${NJOBS} )