Hi All -
What is the process of closing out pull requests on GitHub for extensions
we maintain? For example:
https://github.com/php/pecl-numbers-bitset/issues/11 - I have no way of
closing that out other than to push a bogus commit with "Fix #11" as the
message.
Is there are grant option for GitHub extension maintainers? If so, both PHP
and GH username is willfitch.
Thanks,
Will Fitch
What is the process of closing out pull requests on GitHub for extensions
we maintain? For example:
https://github.com/php/pecl-numbers-bitset/issues/11 - I have no way of
closing that out other than to push a bogus commit with "Fix #11" as the
message.Is there are grant option for GitHub extension maintainers? If so, both PHP
and GH username is willfitch.
Regarding PRs you can use https://qa.php.net/pulls/; choose the repo
and login, and you'll be able to close the PR.
Not sure about issues, though. Probably these shouldn't even be available.
--
Christoph M. Becker
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
Thanks, Johannes. I’ve closed that issue out. Please feel free to turn issues off when you’re able!
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