Revision dd430442aa5c90d95af7766994681aec04c0fddb

Committed on 02/05/2019 6:38 am by André R <ar@ez.no> [GitHub Diff]

Merge branch '1.5'