Merge branch 'release/5.8.0' into develop
authorjenkins <jenkins-int@bgbm.org>
Fri, 19 Jul 2019 13:14:57 +0000 (15:14 +0200)
committerjenkins <jenkins-int@bgbm.org>
Fri, 19 Jul 2019 13:14:57 +0000 (15:14 +0200)

Trivial merge