Merge branch 'master' into githubmaster
authorPhilipp Schüle <p.schuele@metaways.de>
Wed, 13 Jul 2016 09:13:07 +0000 (11:13 +0200)
committerPhilipp Schüle <p.schuele@metaways.de>
Wed, 13 Jul 2016 09:13:07 +0000 (11:13 +0200)

Trivial merge