I have a some files which I want to remove from git, but I don't want the files to be deleted, either locally or on other developers machines.
(These are files which should never have been in the repo, but I hadn't added them to .gitignore in time.)
Currently, my procedure is:
- echo "filename" >> .gitignore
- cp filename filename.safe
- git rm filename
- git commit -a -m"removing filename from repo"
- mv filename.safe filename
- Ask the other developers to cp filename filename.safetoo.
- git push origin main
- Tell the other developers to git pull; mv filename.safe filename.
This procedure is very fragile, requiring correct timing and good communication.
Is there a safer way to remove a file from a git repo, without it being deleted on my machine or others'?
I have seen: Remove a file from a Git repository without deleting it from the local filesystem but my files are already committed and pushed.
