Re: Re: GitHub and Extensions

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. 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