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