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

Minor request: use -Q DIR LP instead of -Q DIR,LP? #215

Closed
cpitclaudel opened this issue Jun 28, 2020 · 2 comments
Closed

Minor request: use -Q DIR LP instead of -Q DIR,LP? #215

cpitclaudel opened this issue Jun 28, 2020 · 2 comments

Comments

@cpitclaudel
Copy link
Collaborator

I'm not sure what the proper way is to do this without breaking existing code. It's just a bit unfortunate that SerAPIs options are not spelled the same as Coq's

@ejgallego
Copy link
Owner

It is indeed a big pain, I tried to have cmdliner to parse that, but I didn't manage to hack a solution where cmdliner would take the arguments in this way, I'll try to re-hack to see what can be done [patches welcome of course]

A likely easier solution would be to have Coq itself take -R log=dir

@ejgallego
Copy link
Owner

coq-lsp auto-configures itself if passed the correct root, so this is less of an issue.

@ejgallego ejgallego closed this as not planned Won't fix, can't repro, duplicate, stale Feb 15, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

2 participants