Closed veksha closed 8 months ago
it's not a new feature. just upgrade to existing one.
readme.txt
already has this section "Server-specific options"
almost all servers are reacting to "workspace/didChangeConfiguration"
notification and "initializationOptions"
.
(this is the same feature but "initializationOptions"
happens on server init only)
jedi server is not reacting to "didChangeConfiguration", only reacts to "initializationOptions". so this can be considered even as bugfix. no need to add anything new to readme.
okay, I got it, thanks...
2024.02.27 (by @veksha)
okay, but user needs some info (in history.txt or readme.txt) HOW to use these IniOpts....