Merge branch 'origin/develop'

This merge does a cleanup of accidentally diverged histories of master
and develop branch.