diff options
| author | DJMcNab <[email protected]> | 2018-12-21 17:00:31 +0000 |
|---|---|---|
| committer | DJMcNab <[email protected]> | 2018-12-21 17:00:31 +0000 |
| commit | 380733d6d0361271620ece87ed970c994fb8b226 (patch) | |
| tree | 5ce8e1c4b820f06f599ea1b1f53faef0161e842b /.gitignore | |
| parent | 70e5fb98a007c49e2f2a1d2f58c31008385c9754 (diff) | |
Undo the previous mistaken change and make publish_decorations optional
See https://github.com/Microsoft/language-server-protocol/issues/567
for motivations to not require `InitializationOptions`
TODO: Check if there are any other protocol extensions
which should be disabled if not implemented on the client
Diffstat (limited to '.gitignore')
0 files changed, 0 insertions, 0 deletions