what's the right procedure when a biggy file (or et of files) get committed (by mistake, for instance), and you want them removed not only from new versions of the git history but from the whole git history to prevent inflating eveyone's repos with biggy files commited by mistake by someone?