Merge branch 'release/5.15.0' into develop
authorjenkins <jenkins-int@bgbm.org>
Tue, 23 Jun 2020 12:31:35 +0000 (14:31 +0200)
committerjenkins <jenkins-int@bgbm.org>
Tue, 23 Jun 2020 12:31:35 +0000 (14:31 +0200)

Trivial merge