Revision b0582eb3fc739fef72209788d0b73e04c9687688

Committed on 09/09/2018 8:03 pm by André R <ar@ez.no> [GitHub Diff]

Merge branch '6.13' into 7.2