Re: Re: GitHub and Extensions

Thanks, Johannes. I’ve closed that issue out. Please feel free to turn issues off when you’re able! > On Oct 7, 2017, at 7:45 AM, Johannes Schlüter <johannes@schlueters.de> wrote: > >> On Fr, 2017-10-06 at 20:11 +0200, Christoph M. Becker wrote: >> >> Not sure about issues, though. Probably these shouldn't even be >> available. >> > > > Correct, usually we disable issues and point users to bugs.php.net to > have a central bug database instead of having to track multiple > trackers. Usually repos are created via a script on https://master.php.��ߒ > &�^�e
��4 > net/manage/github.php which takes care of this. > > We try to limit people with direct access to github repos as direct > pushes there (or clicking the merge button) will break syncing with > git.php.net (to be precise: a push on git.php.net does a force push to > github, which might destroy history) > > Will, I made you collaborator on the repo, so you can respond to the > ticket properly and close it or whatever. A bit later I'll turn issues > of. Please be careful not to directly push to the repo. > > johannes > >