Skip to content
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

Lingering error messages #501

Open
RustanLeino opened this issue Oct 3, 2024 · 1 comment
Open

Lingering error messages #501

RustanLeino opened this issue Oct 3, 2024 · 1 comment

Comments

@RustanLeino
Copy link
Contributor

The error/warning messages reported for a file continue to show in the Problems pane after the file has been closed.

Repro:

  • Open VS Code
  • Open a .dfy file that contains error (or introduce errors in the file after opening it)
  • Close the file
  • The Problems pane still show the errors

Screenshot 2024-10-03 at 14 37 22

@keyboardDrummer
Copy link
Member

I can't reproduce this

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants