GitHub migration complete

[René J.V. Bertin]

Lawrence Velázquez wrote:

...
> $ git gc --aggressive

FWIW, while theoretically very space-efficient, git's .git directories tend to grow to considerable size for active repositories. I find it useful to run the attached script from time to time. It runs the garbage collector, but also (re)packs the remaining data.

R
-------------- next part --------------
#!/bin/sh
# NB: should support repos checked out with --separate-git-dir!
# those have .git as a file containing something like
# gitdir: /path/to/git-dir

if [ ! -d ./.git/ ] ;then
        echo "Not a git repository (./.git/ is not a directory)"
        exit 0
fi

# use a bit of a hack to determine if our stamp exists and is the newest entry in .git
# (using grep to filter out the . and .. entries; this is still faster than running the whole
# operation for nothing).
LASTFILE="`ls -1tra ./.git/ | grep -v '^\.[\.]*$' | tail -1`"
if [ "${LASTFILE}" = ".eradicated" ] ;then
        echo "Nothing changed since last `basename $0` - skipping"
        exit 0
fi

gfilter () {
        echo git filter-branch -f  --index-filter "git rm --force --cached --ignore-unmatch \"$1\"" -- --all
        git filter-branch -f  --index-filter "git rm --force --cached --ignore-unmatch \"$1\"" -- --all
}

for f in $@ ;do
        gfilter "$f"
done

rm -Rf .git/refs/original && \
    git reflog expire --expire=now --all && \
    git gc --aggressive && \
    git prune

date > .git/.eradicated