#git bot interface

History of !branch_rename

• Renaming a branch is easy. `git branch oldname newname`, but this only renames it locally. If you want to rename it globally, you need to `git push origin newname; git push --delete origin oldname` and then users need to `git remote prune origin` and then rename their local branches. Do NOT do this in an attempt to, say, fix a problem on oldname, that is !rewriting_public_history.
  By SethRobertson at 2012-01-06 15:19:56