Revision 3c6b122d2f80655e89aad4cd249d1dc447820119

Committed on 06/08/2018 5:15 am by Marek Nocon <marek.nocon@ez.no> [GitHub Diff]

Merge branch '1.7' into 1.13