Revision e3256ebe75aecb77267c090fcd38aa66b05ee4a4

Committed on 02/12/2018 11:59 am by André R <ar@ez.no> [GitHub Diff]

Merge branch '2017.12' into 2018.09