diff options
| author | Gaëtan Gilbert | 2019-01-22 23:29:28 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-01-22 23:32:46 +0100 |
| commit | 95d977bf0b1825b7d822abbdd062cdb8c38051cb (patch) | |
| tree | 930521bfe8d77d5fc11e42d562ea6607cdfe81ec /dev/ci/ci-wrapper.sh | |
| parent | 03c17218eeacb098ff57ecee1d98f46b7c8fa185 (diff) | |
Remove travis
The azure OSX job replaces the first travis job, and the second always
fails and so is useless.
Diffstat (limited to 'dev/ci/ci-wrapper.sh')
| -rwxr-xr-x | dev/ci/ci-wrapper.sh | 10 |
1 files changed, 1 insertions, 9 deletions
diff --git a/dev/ci/ci-wrapper.sh b/dev/ci/ci-wrapper.sh index 12a70176c2..9ca8f76054 100755 --- a/dev/ci/ci-wrapper.sh +++ b/dev/ci/ci-wrapper.sh @@ -6,13 +6,6 @@ set -eo pipefail -function travis_fold { - if [ -n "${TRAVIS}" ]; - then - echo "travis_fold:$1:$2" - fi -} - CI_NAME="$1" CI_SCRIPT="ci-${CI_NAME}.sh" @@ -22,6 +15,5 @@ cd "${DIR}/../.." export TIMED=1 "${DIR}/${CI_SCRIPT}" 2>&1 | tee time-of-build.log -travis_fold 'start' 'coq.test.timing' && echo 'Aggregating timing log...' +echo 'Aggregating timing log...' python ./tools/make-one-time-file.py time-of-build.log -travis_fold 'end' 'coq.test.timing' |