cleaning repository histories

[danielpeter]

Dear all,
the git history in our repositories has accumulated a lot of file changes over the past decades. This made the .git/ folder pretty large (git count-objects -v -H):

• SPECFEM2D: ~ 349.36 MiB
• SPECFEM3D: ~ 566.09 MiB
• SPECFEM3D_GLOBE: ~1.88 GiB

Cleaning the git history and removing dangling commits as well as large (binary) files that are not in the current repos anymore seems to have become necessary. This will reduce the total size of the git repositories, making the download and cloning much faster again.

However, removing the large and obsolete files will require rewriting the git history, and thus will change commit identifier (SHA1) numbers. It will also impact the forks of the repositories which will need a new rebase.

I would prefer going ahead with cleaning out the histories now before releasing new versions. Please post here any objections or suggestions how to progress.