aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev/ci/ci-math-comp.sh
blob: 2eb150cb524a65769f2c99f28bdf9b65c74e92a3 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
#!/bin/bash

# $0 is not the safest way, but...
ci_dir="$(dirname "$0")"
source ${ci_dir}/ci-common.sh

checkout_mathcomp math-comp

# odd_order takes too much time for travis.
( cd math-comp/mathcomp                           && \
  sed -i.bak '/PFsection/d'                  Make && \
  sed -i.bak '/stripped_odd_order_theorem/d' Make && \
  make Makefile.coq && make -f Makefile.coq -j ${NJOBS} all )