Joerg Thalheim 2a4a1d685d 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.

(cherry picked from commit 44917c46b1)

2017-11-13 20:24:22 +00:00

..

scripts

travis: disable for pull requests

2017-11-13 20:24:22 +00:00