Revision 455b867582c284081103d2b434dd97ca9efc807a

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

Merge branch '8.0'