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 _______________________________________________ ghc-devs mailing list [email protected] http://www.haskell.org/mailman/listinfo/ghc-devs
