Remove files from git repo.

Some files created during the build process should not be added to the git repository, e.g. binary distributions.

But if you added them by mistake, you can remove them with

git rm --cached file0 file1 … filen

since git rm without the --cached would also remove the files form disk.