GitHub pull requests

[Herbert Valerio Riedel]

Hello,

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
>> pull-request.
>
> 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)

Cheers,
  hvr