diff options
| author | Michael Davis | 2022-06-20 23:15:50 +0000 |
|---|---|---|
| committer | GitHub | 2022-06-20 23:15:50 +0000 |
| commit | 0ad10ce6f7159bc857eef1445a6c5cc28ae6a249 (patch) | |
| tree | b5d771c9d52907b26e7e44bf494b7bfaec6b9578 /runtime/queries/lean | |
| parent | 8c64c3dfa3be911344ae0acaeee8018ffccde643 (diff) | |
rewrite language configuration docs (#2838)
This change moves the configuration tables from the Adding
Languages guide into the overall Languages section. It also
adds more detailed documentation on the `language-server`
configuration key and fixes a typo in the "mylang" example
(the scope was `scope.mylang` instead of `source.mylang`).
Diffstat (limited to 'runtime/queries/lean')
0 files changed, 0 insertions, 0 deletions