-
Notifications
You must be signed in to change notification settings - Fork 73
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Characters are lost in the editor when typing fast and DOT parsing errors occur #22
Comments
magjac
added a commit
that referenced
this issue
Aug 29, 2018
This speeds up feedback for erroneus DOT and reduces the risk of triggering #22
magjac
added a commit
that referenced
this issue
Sep 11, 2018
I am still experiencing this. I will try to come back with reproducible examples as I encounter them. One is |
magjac
added a commit
that referenced
this issue
Nov 15, 2023
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
The reason is that the mechanism that inserts the error marker in the editor gutter also re-insert the latest text exported from the editor which might not be up-to-date when typing fast.
The text was updated successfully, but these errors were encountered: