Revision dc447018c32c4af1b3a6a2559ae8168ac58ff1c9

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

Merge branch '7.2'