function git-push-diff-name git push -f origin HEAD:$argv[1] end