Note to myself:
To remove a directory from an existing git repository there are various ways to do it. The obvious way is
$ git filter-branch --tree-filter 'rm -rf directory/'
Which is just fine for smaller repositories but can take a long time on large repositories with a lot of large files in that directory.
The faster way is to manipulate only the index:
git filter-branch --index-filter 'git ls-files -- DIRECTORY | xargs git update-index --remove' --tag-name-filter cat --prune-empty -f -- --all;
- git ls-files will give you a list of files in the DIRECTORY
- git update-index will remove those files from the index
- And the tag filter is there to include tags
- –prune-empty tells filter-branch to ignore empty commits.