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 3 years ago Last modified on Mar 14, 2018, 9:52:51 AM