It was never supposed to be part of the repo, and currently accounts for at least half of the .git directory's size. We need to nip it in the bud before `git clone` times become unmanageable!
