development.7/FILES: add CONTRIBUTING + git-arc.sh
Sorry, forgot working on the branch while PR is closed makes it unopenable.
Sorry, forgot working on the branch while PR is closed makes it unopenable.
Untrue, though it does make the process more difficult. There are two conditions for reopening a closed GitHub pull request:
- The branch name must be the same.
- The branch must point to where it was at when the pull request was closed.
As such you need to save your working location, then recreate the branch where it was at the time of closure (GitHub will happily provide the commit hash; you can simply invoke git push -f github <old_hash>:<old_branch_name>). Then wait 2-5 minutes for things to propagate through GitHub's servers. Then go back to the closed pull request and the option to reopen will be available.
Once reopened you can update in any fashion you desire. Since you've created a new pull request you likely no longer want to do this, but it is entirely possible.
Thanks @ehem! This is great information.