Two way git mirror: Difference between revisions

There is one caveat: Deletion of branches is not mirrored, but deleted branches are resurrected by the mirror script.

To delete a branch for good, the following commands need to be executed in quick succession.

<source lang="bash">

git branch -d [branchName]

git push github --delete [branchName]

git push sourceforge --delete [branchName]

</source>