diff options
| author | Théo Zimmermann | 2017-03-28 18:05:32 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2017-04-06 15:17:00 +0200 |
| commit | e3dc35ad414ce3e554073f8761ec5ca37f367204 (patch) | |
| tree | 292d76238064cd542a062ebdc0a7e6f8e78a725d | |
| parent | 45985baf2262504a9fb8f24e7960caa9f11d29f3 (diff) | |
[travis] Add webhook to Gitter.
| -rw-r--r-- | .travis.yml | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/.travis.yml b/.travis.yml index 81f50af0a0..d35b7a8422 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 |