Revision 24bd53bbd85db8aebb1638b82bab30a791206600

Committed on 17/10/2018 8:29 am by Andrew Longosz <andrzej.longosz@ez.no> [GitHub Diff]

Merge branch '6.13' into 7.2