Merge branch 'master' of https://amos@git.eclipse.org/r/mangrove/org.eclipse.mangrove