branch -d and pushing (Was: Working with Git)

[Jeremy Lavergne]

Ensure you pull or fetch your merged changes otherwise you'll never be
allowed to delete the branch. So if on branch X you have GitHub merge
branch Y, you cannot delete Y until you fetch X.

If we get lots of branches, you can prune remote tracking easily:
git fetch -p

(remember:
 - local tracking "master"
 - remote tracking "origin/master")

On 11/03/2016 11:36 AM, Lawrence Vel�zquez wrote:
> Yeah, you can delete it. You should NOT use "git branch -D" as Sterling
> suggested because these instructions are designed so that you can always
> fast-forward merge the PR branch into master. If "git branch -d" fails,
> something is not right, and you have to go back and figure out what.
> 
> One small addendum: Before "git push origin master", you should run "git
> pull --rebase" to get any new commits that were pushed by other
> committers.