Merge branch 'master' of ssh://idieng@git.eclipse.org/gitroot/sphinx/org.eclipse.sphinx.git