Revision b3f1fa46d10ac568c6554a8ca7158cf09f352635

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

Merge branch '8.0'