Merge branch 'master' into 'dev'

Previous attempts to merge failed due to bugs in merge tools. Performing merge from command line works as expected.
This commit is contained in:
Magne Sjaastad 2019-12-20 09:37:03 +01:00
commit f22161bf6e

Diff Content Not Available