diff options
author | JJ | 2023-12-16 04:29:26 +0000 |
---|---|---|
committer | GitHub | 2023-12-16 04:29:26 +0000 |
commit | c56cd6ee8b9312a620d4fc38eea90a49613f5d72 (patch) | |
tree | ce90625c3fd89600368114697d7f9af0b7173d07 /book/src/generated | |
parent | 914c83420b9901f596bf771ad5f20495de9a070c (diff) |
Add support for Agda (#8285)
* agda language support (wip)
* improve highlights
* disable agda-language-server
* minor addendum to documentation
* cargo xtask docgen
* oh i can just do this neat
* minor comment cleanup
* upstream updated
* imports: missed a spot
---------
Co-authored-by: Michael Davis <mcarsondavis@gmail.com>
Diffstat (limited to 'book/src/generated')
-rw-r--r-- | book/src/generated/lang-support.md | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/book/src/generated/lang-support.md b/book/src/generated/lang-support.md index 1fad1017..0ec8f5ba 100644 --- a/book/src/generated/lang-support.md +++ b/book/src/generated/lang-support.md @@ -1,5 +1,6 @@ | Language | Syntax Highlighting | Treesitter Textobjects | Auto Indent | Default LSP | | --- | --- | --- | --- | --- | +| agda | ✓ | | | | | astro | ✓ | | | | | awk | ✓ | ✓ | | `awk-language-server` | | bash | ✓ | ✓ | ✓ | `bash-language-server` | |