On 1/25/2018 1:53 PM, Brett Cannon wrote: > I would assume it would just go into miss-islington, but before we get > ahead of ourselves and design this we need to get consensus that people > like the overall idea of using a bot to do a main commits as well. I strongly dislike any idea of making me do more error-prone work when merging. Also, pressing the big green button is a distinct action from anything else one does on the page. I am sure this is intentional from a UI design viewpoint, to minimize the possibility of merging by accident. I am personally not so concerned about changing '#' to 'GH-'. The bpo number is already distinguished by the 'bpo-' prefix. But since you are: Supposes when a PR is created, a bot appended '(GH-nnnn)' to the title. Would github's bot still append '(#nnnn)'? What is it appended '(GH#nnnn)'? Can titles be edited by a bot after a merge? (You might want this anyway to 'correct' existing merges.) Can we ask GH to make the number prefix a configuration option? -- Terry Jan Reedy
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4