This file should be deleted. I believe I've deleted it before, so it might have snuck back.
Sometimes git gets confused with deleted files. Just make sure it's gone on your end before you push and it should be fine. But it might accidentally re-appear in a PR so we should try to watch out for it.
This file should be deleted. I believe I've deleted it before, so it might have snuck back.
Sometimes git gets confused with deleted files. Just make sure it's gone on your end before you push and it should be fine. But it might accidentally re-appear in a PR so we should try to watch out for it.