blob: a5b3b1491d52a14dfa8ae9fded094fe0e486ce07 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
|
CI_TARGETS=ci-all \
ci-bignums \
ci-color \
ci-compcert \
ci-coq-dpdgraph \
ci-coquelicot \
ci-cpdt \
ci-fiat-crypto \
ci-fiat-parsers \
ci-flocq \
ci-formal-topology \
ci-geocoq \
ci-hott \
ci-iris-coq \
ci-math-classes \
ci-math-comp \
ci-metacoq \
ci-sf \
ci-tlc \
ci-unimath \
ci-vst
.PHONY: $(CI_TARGETS)
# Generic rule, we use make to easy travis integraton with mixed rules
$(CI_TARGETS): ci-%:
+./dev/ci/ci-pipe-tee.sh ./dev/ci/ci-$*.sh time-of-build.log
echo 'Aggregating timing log...' && echo -en 'travis_fold:start:coq.test.timing\\r'
python ./tools/make-one-time-file.py time-of-build.log
echo -en 'travis_fold:end:coq.test.timing\\r'
|
