Pretend you never pushed that file in git

Years ago, when I was starting to use git, I commited (and pushed) a file I didn't want. It was a huge TAGS file, which made the repo unusable.

 At that time I found a way to remove it, but today I stumbled upon a github page which explains it way better.

Enjoy