aboutsummaryrefslogtreecommitdiffhomepage
path: root/.travis.yml
diff options
context:
space:
mode:
authorGravatar Théo Zimmermann <theo.zimmi@gmail.com>2017-03-28 18:05:32 +0200
committerGravatar Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>2017-04-06 15:17:00 +0200
commite3dc35ad414ce3e554073f8761ec5ca37f367204 (patch)
tree292d76238064cd542a062ebdc0a7e6f8e78a725d /.travis.yml
parent45985baf2262504a9fb8f24e7960caa9f11d29f3 (diff)
[travis] Add webhook to Gitter.
Diffstat (limited to '.travis.yml')
-rw-r--r--.travis.yml9
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