Lessons Learned from the move to GitHub

Repository Conversion

Pull Requests

  • The bot is very helpful, and so is the GitHub UI for merging things easily without having to use a command line.
  • pmetzger is doing a great job in keeping the number of open pull requests down
  • Only members can be assigned to pull requests in GitHub, but we have non-member maintainers. We should change the bot to assign the PRs if the maintainers are members, but keep the current behavior to also support the use case for external maintainers.
  • We may have a bit of a hot trigger finger when merging pull requests, but that does not seem to have caused problems so far, so it's likely a non-issue.
  • We can now request reviews before merging changes and are using this quite a bit on base and infrastructure repositories.

GitHub handles in Portfiles #56050

  • A lot of maintainers have not added their GitHub handle to Portfiles, even regular contributors.
  • We could use the Trac database to compute a match and automate the task.
  • We should probably make Trac always use email addresses from GitHub and remove the ability to change email addresses in Trac.


Last modified 21 months ago Last modified on Mar 14, 2018, 9:52:51 AM