Script to permanently remove paths from git's tree and index.

git-remove-permanently.sh

#!/bin/bash
#
# Removes the given paths permanently from the git index and tree.
#
set -e

function stats {
    echo
    echo "Git Objects:"
    git count-objects -v
    echo
    echo "Repository size: "
    du -hs .git | cut -c 2-5
    echo
}

if [ $# -eq 0 ]; then
    echo "Usage: $0 <path1> <path2> ..."
    exit 0
fi
 
if [ ! -d .git ]; then
    echo "The script must run inside the parent directory of a .git/ repo."
    exit 1
fi

stats

paths=$@
git filter-branch -f --index-filter "git rm -rf --cached --ignore-unmatch $paths" HEAD
git filter-branch -f --tree-filter "rm -rf $paths" HEAD
rm -rf .git/refs/original/
git reflog expire --all
git gc --aggressive --prune

stats

echo "Done."