The repo history has two large files in it:
de436t.bsp, which are no longer in the repo (as of commit 49a80684b072a28471d7c3c1d09832c1bfcf8805), but are still in the history. Would it be possible to remove these files completely from the git history? This can be done easily and safely with BFG, e.g. (from one directory below the tempo2 repository directory):
java -jar bfg-1.12.15.jar --delete-files *.bsp tempo2 cd tempo2 git reflog expire --expire=now --all && git gc --prune=now --aggressive git push
The main reason I ask is that I've got a mirror of tempo2 on github and each time I update it after rebasing to this repo I have to run the above commands, otherwise github complains about the large files. Also, I imagine it would be a good way to generally de-bloat the repo history.