I need to make the repo smaller. I think I can make it smaller by removing problematic binary files from git history:
git filter-branch --index-filter 'git rm --cached --ignore-unmatch BigFile'
And then releasing the objects:
rm -rf .git/refs/original/
git reflog expire --expire=now --all
git gc --aggressive --prune=now
(Feel free to comment if those commands are wrong.)
The problem: How to identify those big files so that I can asses whether to remove them from git history? Most likely they are not in the working tree anymore - they have been deleted and probably also untracked with:
git rm --cached BigFile