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