git-remove-from-history

# Based on:
# https://confluence.atlassian.com/bitbucket/reduce-repository-size-321848262.html

for m in "$@" ; do  # jscoq/coq-pkgs/*.coq-pkg ; do
git filter-branch --index-filter "git rm --cached --ignore-unmatch $m" HEAD
git for-each-ref --format="%(refname)" refs/original/ | xargs -n 1 git update-ref -d
done

# Prune all of the reflog references from now on back (unless you're explicitly only operating on one branch).
git reflog expire --expire=now --all
# Repack the repository by running the garbage collector and pruning old objects.
git gc --prune=now
# Push all your changes back to the remote repository.
git push --all --force
# Make sure all your tags are current too:
git push --tags --force