Wiping a (large) file from a git repository
Issue
You might have a file in a repository, which you want to delete because it is too large (or because it contains passwords, etc.).
Solution
General principle
The following procedure will wipe a file from your repository and compress it, so your repository will be reduced in size. It will not delete your work copy.