I changed the name of a file and then renamed to the original name again, and this happens:  The old file still appears as a candidate to go to. #### Versions - OS: Windows 10. - PHP Version: 7.3.7. - VSCode: 1.38.1. - Tenkawa plugin: 0.4.4.