Remove the binary file lib/frege*.jar from the repo

[mperry]

I tried to remove the jar file from the repo. The following command shows the large files:

git verify-pack -v .git/objects/pack/*.idx | sort -k 3 -n | tail -5

I am not sure if it is removed or not. Can a clever person go and look and remove the jar file from the git history if not already done?

[mperry]

I used the BFG repo cleaner (https://rtyley.github.io/bfg-repo-cleaner/) and think I have solved the problem. I ran:

git clone --mirror git://github.com/Frege/frege-interpreter.git
java -jar bfg-1.12.6.jar  --strip-blobs-bigger-than 2M frege-interpreter.git/
cd frege-interpreter.git
git reflog expire --expire=now --all && git gc --prune=now --aggressive
git push  https://github.com/Frege/frege-interpreter.git --force

The most interesting part of running bfg was the output:

Deleted files
-------------

    Filename                      Git id            
    ------------------------------------------------
    frege-3.23.370-g898bc8c.jar | d8053163 (22.0 MB)

In total, 3 object ids were changed. Full details are logged here:

    /media/sf_D_DRIVE/repositories/frege-interpreter.git.bfg-report/2015-10-22/21-49-17

BFG run is complete! When ready, run: git reflog expire --expire=now --all && git gc --prune=now --aggressive

Now when I clone the github repo and run: git verify-pack -v .git/objects/pack/*.idx | sort -k 3 -n | tail -5

I get:

1bb8fff7f751278187a79ada0452d1098e69a7b3 blob   13530 5313 151743 1 65973c287fc32e3dac5a11297d0143fd10061447
0cf5533dfa2fe17637e0c812fcb2122152062508 blob   14959 3881 42760
dc63e960c8846dc6386ee137c189cba09afd9e7a blob   27358 8604 31631
65973c287fc32e3dac5a11297d0143fd10061447 blob   29959 8081 143662
3d0dee6e8edfecc92e04653ec780de06f7b34f8b blob   51017 45637 56616

The file sizes look right now.

[mperry]

We need someone to double check what I have done. Once this is confirmed as ok, we need everyone to delete local repos and clone again from Github. We don't want the large binary files to be exploding the size of the repo.

[mperry]

@mmhelloworld and @Dierk, can you check what I have done?

[mmhelloworld]

We can delete the local jar. It was just a temporary solution until the latest frege was available on maven central. I already removed it from the build but forgot to remove the local jar. Thanks for looking into this!