A colleague has done a few things I told them not to do:

• forked the origin repo online
• cloned the fork, added a file that shouldn't have been added to that local repo
• pushed this to their fork

I've then:

• merged the changes from the fork and found the file

I want to remove this from:

• my local repo
• the fork
• their local repo

I have a solution for removing something from the history, taken from Remove file from git repository (history). What I need to know is, should my colleague also go through this, and will a subsequent push remove all info from the fork? (I'd like an alternative to just destroying the fork, as I'm not sure my colleague will do this)

SOLUTION: This is the shortest way to get rid of the files:

check .git/packed-refs - my problem was that I had there a refs/remotes/origin/master line for a remote repository, delete it, otherwise git won't remove those files
(optional) git verify-pack -v .git/objects/pack/#{pack-name}.idx | sort -k 3 -n | tail -5 - to check for the largest files
(optional) git rev-list --objects --all | grep a0d770a97ff0fac0be1d777b32cc67fe69eb9a98 - to check what files those are
git filter-branch --index-filter 'git rm --cached --ignore-unmatch file_names' - to remove the file from all revisions
rm -rf .git/refs/original/ - to remove git's backup
git reflog expire --all --expire='0 days' - to expire all the loose objects
(optional) git fsck --full --unreachable - to check if there are any loose objects
git repack -A -d - repacking the pack
git prune - to finally remove those objects