diff options
Diffstat (limited to 'dev/ci/ci-coquelicot.sh')
| -rwxr-xr-x | dev/ci/ci-coquelicot.sh | 27 |
1 files changed, 5 insertions, 22 deletions
diff --git a/dev/ci/ci-coquelicot.sh b/dev/ci/ci-coquelicot.sh index 4a23e51be..40eff03b7 100755 --- a/dev/ci/ci-coquelicot.sh +++ b/dev/ci/ci-coquelicot.sh @@ -1,29 +1,12 @@ -#!/bin/bash +#!/usr/bin/env bash -# $0 is not the safest way, but... ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh -git clone --depth 3 https://github.com/math-comp/math-comp.git +Coquelicot_CI_DIR=${CI_BUILD_DIR}/coquelicot -# coquelicot just needs mathcomp -( cd math-comp/mathcomp && \ - sed -i.bak '/ssrtest/d' Make && \ - sed -i.bak '/odd_order/d' Make && \ - sed -i.bak '/all\/all.v/d' Make && \ - sed -i.bak '/character/d' Make && \ - sed -i.bak '/real_closed/d' Make && \ - sed -i.bak '/solvable/d' Make && \ - sed -i.bak '/field/d' Make && \ - sed -i.bak '/fingroup/d' Make && \ - sed -i.bak '/algebra/d' Make && \ - make -j ${NJOBS} && make install ) +install_ssreflect -# Setup ssr -# echo "Add ML Path \"`pwd`/math-comp/mathcomp/\"." > ${HOME}/.coqrc -# echo "Add LoadPath \"`pwd`/math-comp/mathcomp/\" as mathcomp." >> ${HOME}/.coqrc +git_checkout ${Coquelicot_CI_BRANCH} ${Coquelicot_CI_GITURL} ${Coquelicot_CI_DIR} -# Setup coquelicot -git clone --depth 3 https://scm.gforge.inria.fr/anonscm/git/coquelicot/coquelicot.git - -( cd coquelicot && ./autogen.sh && ./configure && ./remake -j${NJOBS} ) +( cd ${Coquelicot_CI_DIR} && ./autogen.sh && ./configure && ./remake -j${NJOBS} ) |