aboutsummaryrefslogtreecommitdiff
path: root/languages.toml
diff options
context:
space:
mode:
authorMatthew Toohey2022-07-05 11:00:38 +0000
committerGitHub2022-07-05 11:00:38 +0000
commitd78354c537e00ddb0976efad1df49c90a224f107 (patch)
tree0295e84bda9b8df88bd8db2d560cd974dd80bf1c /languages.toml
parentb26e7e2e8fc900b5637d9772ecb74874e8794ecc (diff)
add language `idris` (#2971)
Diffstat (limited to 'languages.toml')
-rw-r--r--languages.toml11
1 files changed, 11 insertions, 0 deletions
diff --git a/languages.toml b/languages.toml
index 7c63c051..9da454a0 100644
--- a/languages.toml
+++ b/languages.toml
@@ -1503,3 +1503,14 @@ grammar = "elvish"
[[grammar]]
name = "elvish"
source = { git = "https://github.com/ckafi/tree-sitter-elvish", rev = "e50787cadd3bc54f6d9c0704493a79078bb8a4e5" }
+
+[[language]]
+name = "idris"
+scope = "source.idr"
+injection-regex = "idr"
+file-types = ["idr"]
+shebangs = []
+roots = []
+comment-token = "--"
+indent = { tab-width = 2, unit = " " }
+language-server = { command = "idris2-lsp" }