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.
Trac
Download in other formats: