osdir.com

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Python-Dev] GH-NNNN vs #NNNN in merge commit


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