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
