Removing a directory from a git repository the fast way
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. [...]