Merge "Merge branch release-5-1 into release-2016" into release-2016
authorDavid van der Spoel <davidvanderspoel@gmail.com>
Fri, 8 Jul 2016 14:24:25 +0000 (16:24 +0200)
committerDavid van der Spoel <davidvanderspoel@gmail.com>
Fri, 8 Jul 2016 14:24:25 +0000 (16:24 +0200)

Trivial merge