Filter out plugins from git repository?

Should we remove all commits to do with plugins, now that they are in their own repositories? git filter-branch --tree-filter 'rm -fr bot' --prune-empty HEAD should do the trick.