Remove de435t.bsp and de436t.bsp from repo history

[Matt Pitkin]

The repo history has two large files in it: de435t.bsp and 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.

[Michael Keith]

Perhaps in general we should move to remove the ephemerides from the repo. I'll have a look at your suggestion, though generally I am not keen to much around with the version history.

[Matt Pitkin]

Thanks. When I've used BFG it's been safe and not touched anything else in the history, but it's not a major issue if this isn't removed.

Probably the ephemerides should be removed from the repo and maybe re-added using git lfs.

[Michael Keith]

So I've looked at this and it seems like a good idea, except it seems like it forces everyone to clone a fresh copy of the repo.

I'll contact the other people with write permissions and see what the consensus is.