Opened 7 years ago
Last modified 7 years ago
#823 closed task
Tweak GitHub mirror settings — at Version 1
| Reported by: | mloskot | Owned by: | mloskot |
|---|---|---|---|
| Priority: | major | Milestone: | |
| Component: | Default | Version: | |
| Severity: | Unassigned | Keywords: | git, github |
| Cc: |
Description (last modified by )
Although we agreed to accept contributions via GitHub, it needs extra care to be taken.
GEOS on GitHub does:
- Allow pull requests
- Disallow merging with the green button on GitHub
Possibly, the mirror repo settings needs to be tweaked to support this workflow.
GitHub mirror is updated with git push --mirror destroying any branch which is not in the upstream (gogs). So, PRs must be submitted from contributor's own fork to avoid feature branches destruction.
Note:
See TracTickets
for help on using tickets.
