[Repo] Decrease size of Git repository
The repository is now over 2GB large. We should think about cutting down the size, by rewriting the history: https://github.com/newren/git-filter-repo
The repository is now over 2GB large. We should think about cutting down the size, by rewriting the history: https://github.com/newren/git-filter-repo