GitHub pull requests
Herbert Valerio Riedel
hvriedel at gmail.com
Sun Oct 5 12:11:26 UTC 2014
On 2014-10-05 at 14:03:41 +0200, Joachim Breitner wrote:
> Am Sonntag, den 05.10.2014, 13:08 +0200 schrieb Herbert Valerio Riedel:
>> On 2014-10-05 at 12:56:28 +0200, Joachim Breitner wrote:
>> > I think the advantage could outweigh the downside and it’s worth a try.
>> > We don’t even have to advocate it aggressively, just remove the „Do not
>> > submit PRs“ notice on the repo and see what happens.
>> > (The problem with the ticket numbers remain, unfortunately.)
>> Take into account though, there's no easy going back once we open that
>> Pandora box; once GitHub allocates a #-number for a repo, it can only be
>> removed by involving the GitHub admins, and until then any overlapping
>> #-reference will lead to confusing notifications and ticket/issue
>> comments associated w/ the respective Trac-ticket and/or GitHub
> that’s a valid point.
> Is there maybe a way to disable all #-number-parsing on GitHub? But I
> haven’t seen it...
Not that I know of; I'd be a bit suprised though if it was indeed
possible, as it's a core feature of GitHub (and after all, you can't
disable the PR-submission either)
More information about the ghc-devs