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

(Some?) Warning settings from _CoqProject are ignored #1041

Open
Blaisorblade opened this issue Feb 19, 2025 · 2 comments
Open

(Some?) Warning settings from _CoqProject are ignored #1041

Blaisorblade opened this issue Feb 19, 2025 · 2 comments

Comments

@Blaisorblade
Copy link
Contributor

_CoqProject:

-arg -w -arg -cannot-open-path

Result:
Image

RIght now, I'm not seeing this on Rocq master, but I see it on an older snapshot, but I'm not sure how well this generalizes.

@gares
Copy link
Member

gares commented Feb 19, 2025

Where is the _CoqProject?
On roc-master vscoq should use the one closest to the file, while on older versions it was using only the one at the root of the workspace.

@Blaisorblade
Copy link
Contributor Author

It's at the root of the workspace — with no other one available on the path to it, so that both methods should find the same file...

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