Revision 6a271eb3f48690694d17b6e999567bc21bbe574b

Committed on 03/03/2020 7:45 am by Gunnstein Lye <[email protected]> [GitHub Diff]

Merge branch '2017.12' into 2019.03