Revision 6235ed0afdb44c1eced6998b05d90f02730a527a

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

Merge branch '7.5' into 8.0