From baa072b249f9d084fea5c29bf551d4191261d314 Mon Sep 17 00:00:00 2001 From: Hrvoje Jasak Date: Fri, 4 Feb 2011 13:30:45 +0000 Subject: [PATCH] Update, David Boger --- HowToContribute | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/HowToContribute b/HowToContribute index 1afd33360..674db4a5f 100644 --- a/HowToContribute +++ b/HowToContribute @@ -100,6 +100,19 @@ git Repository: Henrik Rusche (h.rusche@wikki.co.uk) branch, and then delete the branch from the server, as it is no longer needed once it has been merged. + If you need to delete the branch from the server or are requested to do so, the proper + command is + + + git push origin :my-feature-branch + + To delete the same branch from your local repository requires the command + + + git branch -d my-feature-branch + + Finally, to clean your local repository of tracking branches that have been deleted + from the server requires the command + + + git remote prune origin 5. git Commit Policies and Workflow (Committee Perspective) ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~