Describe the bug
Git clone requires a lot of time and disk space due to two binary files accidentally checked in a while back.
Proposed solution: force push.
To Reproduce
Steps to reproduce the behavior:
git clone
du -h
Expected behavior
Smaller disk usage.