Revision e720d3f71c49131e911a4344030e314841448c3d

Committed on 17/02/2019 12:12 am by Sebastian Bergmann <sb@sebastian-bergmann.de> [GitHub Diff]

Merge branch '7.5' into 8.0