diff options
author | Théo Zimmermann <theo.zimmi@gmail.com> | 2017-03-28 18:05:32 +0200 |
---|---|---|
committer | Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2017-04-06 15:17:00 +0200 |
commit | e3dc35ad414ce3e554073f8761ec5ca37f367204 (patch) | |
tree | 292d76238064cd542a062ebdc0a7e6f8e78a725d /.travis.yml | |
parent | 45985baf2262504a9fb8f24e7960caa9f11d29f3 (diff) |
[travis] Add webhook to Gitter.
Diffstat (limited to '.travis.yml')
-rw-r--r-- | .travis.yml | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/.travis.yml b/.travis.yml index 81f50af0a..d35b7a842 100644 --- a/.travis.yml +++ b/.travis.yml @@ -123,3 +123,12 @@ script: - echo 'Running tests...' && echo -en 'travis_fold:start:coq.test\\r' - ${TW} make -j ${NJOBS} ${TEST_TARGET} - echo -en 'travis_fold:end:coq.test\\r' + +# Testing Gitter webhook +notifications: + webhooks: + urls: + - https://webhooks.gitter.im/e/3cdabdec318214c7cd63 + on_success: change # options: [always|never|change] default: always + on_failure: always # options: [always|never|change] default: always + on_start: never # options: [always|never|change] default: always |