-
Notifications
You must be signed in to change notification settings - Fork 57
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
sharing config between client and server #432
Conversation
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
How about adding the config to the example-project
as an example.
Also, should the README be updated.
Updated the readme. Can't set up the configuration in the example project though, because VSCode doesn't save settings in the repo by default. |
Thanks! Merging. |
Nit: does not look like changing the setting and restarting the server picks them up. |
You mean when restarting via the restart command recently added? |
yes |
Or I guess the more general question is: why polling. If one needs to restart anyway. |
Hmm, I don't need to restart anything, polling works fine for me as I tested. How are you testing it? |
What I've tried is: change the setting, then ask the server to restart. |
Don't know what else to test without restarting the entire editor. |
Ahh, I think I know the issue. I'll fix it. |
Done here: #438 |
Fixes #23
This introduces configuration in the extension, periodically synced to the language server for use. We'll probably need to revisit this if we get more intricate configuration needs later on, but for now this is simple enough and will do for the cases we currently have.