#git bot interface

History of !branch_delete

• Deleting a branch is easy. `git branch -d branchname` (or -D). However, this will NOT delete the branch upstream, that requires `git push --delete origin branchname`. However, this will NOT delete remote tracking branches. EACH USER must `git remote prune origin`, but if any users have local branches, they must likewise run `git branch -d branchname` (or -D)
  By SethRobertson at 2012-01-06 15:13:53
• Deleting a branch is easy. `git branch -d branchname` (or -D depending). However, this will NOT delete a branch upstream. To do that you must push the deletion. `git push --delete origin branchname`. However, this will NOT delete remote tracking branches with that name. To do that EACH USER must `git remote prune origin``. However, this will NOT delete any local tracking branches other users
  By SethRobertson at 2012-01-06 15:10:44