I have a very basic knowledge of git

Looking to remove files from git history, team has been pushing large .CSV to the repo for months (because the extension was in caps they went through the .gitignore...)

I tried to delete the files with git filter then with the python add-on filter-repo

approach 1

git filter-branch —-force —index-filter \
“git rm —cached —ignore-unmatch -r‘\*.CSV’” \
—prune-empty —tag-name-filter cat — —all

approach 2

$ git gc
$ git filter-repo --replace-refs delete-no-add --strip-blobs-bigger-than $ 50M
$ git reflog expire --expire=now --all
$ git gc --aggressive --prune=now

checking with du -sh .git, the size goes from 2GB to 400MB

usual next steps I read was to push origin master -f but my admin prevents from pushing to master, so I'm at a loss at how to update the remote repo from either approach?

I tried doing the same steps on a branch and making a PR to no avail

-----Edit-----

Thanks for confirming there was no other way than pushing to master, Admin pushed for me -- life is good

CodePudding user response：

You are going to need to work with your admin to allow a push to master in this case. This is something that you are going to want to coordinate with the team anyway. Removing the file from the repo's history, changes the commits and can lead to some complications with the feature branches.