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-%: rm -f ci-$*.ok +(./dev/ci/ci-$*.sh 2>&1 && touch ci-$*.ok) | tee 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' rm ci-$*.ok # must not be -f; we're checking to see that it exists