Purge file from git history. Useful if like me you commit/push sensitive data, aka credentials. Command was copied from the excellent Github article: https://help.github.com/articles/remove-sensitive-data

purge_file_git_repo.md

1. Change into repo folder

cd my-repo

2. Change into branch you want to modify if not already in it

git checkout <branch>

3. Purge the file

This is the nuclear option. Have to be sure this is what is wanted! Substitute with the name of the file you want gone!

git filter-branch --force --index-filter \
 'git rm --cached --ignore-unmatch <filename>' \
 --prune-empty --tag-name-filter cat -- --all

4. Push back into remote

git push origin <branch>