Revision 8b99091782a5a1c677c1c2bfa40580c1c53df495

Committed on 05/12/2018 5:49 am by Gunnstein Lye <gunnstein.lye@ez.no> [GitHub Diff]

Merge branch '7.2' into 7.3