Revision 2d65122d94ee651255b80cead302adf8178aff54

Committed on 14/02/2019 11:52 pm by Sebastian Bergmann <sb@sebastian-bergmann.de> [GitHub Diff]

Merge branch '7.5' into 8.0