We have a workflow step of changing ‘#’ to ‘GH-’ when we merge pull requests on GitHub. Originally this was implemented to namespace GitHub issue numbers so that if/when we migrate to another tool the commit messages are unambiguous as to what issue on what platform they are linked to.
As I still from time to time forget to change ‘#’ to ‘GH-’ and I see that other committers forget that too, I’m wondering if we just stop doing this. Hence this poll!
- Keep the current workflow: change ‘#123’ to ‘GH-123’ on every PR merge
- Simplify the merge workflow and keep commit messages as GitHub suggests