Opened 7 years ago
Last modified 7 years ago
#823 closed task
Tweak GitHub mirror settings — at Version 2
| 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.
Work with Mirror on GitHub
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.
Settings for Mirror on GitHub
# Configure Protected Branches # Disable Merge Button until commit changes are approved by a peer
Change History (3)
comment:1 by , 7 years ago
| Description: | modified (diff) |
|---|
comment:2 by , 7 years ago
| Description: | modified (diff) |
|---|
by , 7 years ago
| Attachment: | geos-github-settings.png added |
|---|
Note:
See TracTickets
for help on using tickets.
Suggested settings for GitHub protected branches