Revision e5712059f601b0441782b3975c43a83f0f974bce

Committed on 13/12/2018 11:15 pm by Marek Nocon <marek.nocon@ez.no> [GitHub Diff]

Merge branch '1.5' into 1.11