Revision f574d49de24ca649d909d6b8c6622ec973838a76

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

Merge branch '8.0'