Skip to content

Commit

Permalink
remove ' and add ⟨⟩ in lean autopairs (helix-editor#10688)
Browse files Browse the repository at this point in the history
  • Loading branch information
ashl3y-v authored and Vulpesx committed Jun 7, 2024
1 parent bb0f005 commit 4dbfa9d
Showing 1 changed file with 7 additions and 0 deletions.
7 changes: 7 additions & 0 deletions languages.toml
Original file line number Diff line number Diff line change
Expand Up @@ -1040,6 +1040,13 @@ block-comment-tokens = { start = "/-", end = "-/" }
language-servers = [ "lean" ]
indent = { tab-width = 2, unit = " " }

[language.auto-pairs]
'(' = ')'
'{' = '}'
'[' = ']'
'"' = '"'
'⟨' = ''

[[grammar]]
name = "lean"
source = { git = "https://github.com/Julian/tree-sitter-lean", rev = "d98426109258b266e1e92358c5f11716d2e8f638" }
Expand Down

0 comments on commit 4dbfa9d

Please sign in to comment.