Text entered gets inserted in wrong file

[btj]

How to reproduce:

I typed . on model-checking/verify-rust-std#507 and, in the resulting editor, opened verifast-proofs/setup-verifast-home. I then put the cursor at the end of line 20 and typed some text, e.g. foobar followed by Enter.

Expected behavior:

The text gets inserted at the end of line 20 in verifast-proofs/setup-verifast-home.

Observerd behavior:

The text gets inserted in a completely different place, in .github/workflows/update-subtree.yml, on line 217.

Version: 1.108.1
Commit: 585eba7
User Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10_15_7) AppleWebKit/605.1.15 (KHTML, like Gecko) Version/26.2 Safari/605.1.15
Embedder: github.dev

[lszomoru]

/gifPlease

[vs-code-engineering]

Thanks for reporting this issue! Unfortunately, it's hard for us to understand what issue you're seeing. Please help us out by providing a screen recording showing exactly what isn't working as expected. While we can work with most standard formats, .gif files are preferred as they are displayed inline on GitHub. You may find https://gifcap.dev helpful as a browser-based gif recording tool.

If the issue depends on keyboard input, you can help us by enabling screencast mode for the recording (Developer: Toggle Screencast Mode in the command palette). Lastly, please attach this file via the GitHub web interface as emailed responses will strip files out from the issue.

Happy coding!

[jruales]

@btj I'm not able to repro. Did you wait until the PR was loaded before editing verifast-proofs/setup-verifast-home? What I see is that after a little wait, the "Changes in Pull Request" tab opens up with the changes from the PR.

Maybe it was just a coincidence that that editor opened up just as you started typing in verifast-proofs/setup-verifast-home?