diff options
| author | Maxime Dénès | 2017-04-06 15:51:29 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-04-06 15:51:29 +0200 |
| commit | 91b82f5a7b3cff65aeadd7c8323d63bf91b5f2e1 (patch) | |
| tree | a685f3f177efbc1ee66e39245d4b96376fd679e7 | |
| parent | 9f188da28f65341f5c5ecd0b3b4f9b447bbc2b15 (diff) | |
| parent | e3dc35ad414ce3e554073f8761ec5ca37f367204 (diff) | |
Merge PR#542: [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 |