Merging github pull request, occasionally accepted directly in github repository