On 11/03/12 00:01, Steve Bennett wrote:
On Sat, Mar 10, 2012 at 6:41 PM, Tom Hughes<t...@compton.nu> wrote:
I would just delete them once they aren't needed anymore.
Delete them locally, you mean? Do you then need to push the deletion?
Well the two things actually separate.
You can delete a local branch with "git branch -d <name>" and a remote
branch by pushing with "git push <remote> :<branch>".
Tom
--
Tom Hughes (t...@compton.nu)
http://compton.nu/
_______________________________________________
Potlatch-dev mailing list
Potlatch-dev@openstreetmap.org
http://lists.openstreetmap.org/listinfo/potlatch-dev
