Joerg Thalheim 44917c46b1 travis: disable for pull requests ...

travis is too slow for us and confuse contributors, who think they have
to get travis tests green.
We have now pr bots instead.

2017-11-13 11:40:42 +00:00

..

scripts

travis: disable for pull requests

2017-11-13 11:40:42 +00:00