Completely remove a file from git history

undo_git.sh

# Remove a commit from git history

## Detach from the remote
git remote rm origin

## Make necessary changes. If you want to keep a file locally but not remotely:
git rm --cached $FILE
echo $FILE >> .gitignore
git add .gitignore

## Or, if you want to remove a file completely:
rm -rf $FILE

## Rewrite history
git filter-branch --index-filter 'git rm --cached --ignore-unmatch $FILE' HEAD

## Then do:
git reflog expire --expire=now --all && git gc --prune=now --aggressive

## Reattach the remote, push the current branch
git remote add origin $YOUR_GIT_REMOTE_URL
git push -u origin `git branch | grep \* | cut -d ' ' -f2`

## If `git pull` fails, you might have to reset the tracking information for the current branch
git branch --set-upstream-to=origin/`git branch | grep \* | cut -d ' ' -f2` `git branch | grep \* | cut -d ' ' -f2`