Two way git mirror: Difference between revisions

Content deleted Content added
imported>Hendrik Brummermann
No edit summary
imported>Hendrik Brummermann
Line 97:
== Deleting branches ==
 
There is one caveat: Deletion of branches is not mirrored, but deleted branches are resurrected by the mirror script.
{{TODO|deleting branches}}
 
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>