The "free" account on github at least doesn't allow, when one has made
a PR that had been merged, to sync the branch: the commits get in the
way.
I found this solution (browsing) and it seems to work:
- Once a PR has been merged (and I have done nothing more on my
branch), I invoke locally (unix like syntax):
git reset --hard HEAD~1 # of course, could be ~n depending on #commits
then:
git push origin HEAD --force
to update remote. I am then able to sync and to pull on the branch
locally to restart:
git pull
This avoids multiplying branches.
FWIW,
--
Thierry Laronde <tlaronde +AT+ kergis +dot+ com>
http://www.kergis.com/
http://kertex.kergis.com/
Key fingerprint = 0FF7 E906 FBAF FE95 FD89 250D 52B1 AE95 6006 F40C
------------------------------------------
9fans: 9fans
Permalink:
https://9fans.topicbox.com/groups/9fans/Tace9421b32f94a2d-M3d1a9bfa3990413f25bfdf3b
Delivery options: https://9fans.topicbox.com/groups/9fans/subscription
