I wanted to stop tracking a file, so I added it to .gitignore
and did git rm --cache thefile.php
to try to accomplish that. All seemed well. The file remained, but was no longer tracked. I pushed to Github.
Now another machine with the repo has pulled from Github and seen this:
root@server [/home/butkus/public_html]# git pull
Password for 'https://billybutkus@github.com':
Updating 42e1727..2e0aef4
Fast-forward
.../path/to/file.php | 13 -------------
1 file changed, 13 deletions(-)
delete mode 100644 path/to/file.php
root@server [/home/butkus/public_html]#
File is now actually deleted rather than just ignored. What did I do wrong?
This amazingly well upvoted answer tells me I did it exactly right: https://stackoverflow.com/a/1143800/631764
But I sure didn't.