add ruler at 101 and text-width at 100 to lean in languages.toml (#10969)

This commit is contained in:
Ashley Vaughn 2024-06-22 18:09:39 -07:00 committed by GitHub
parent b894cf087b
commit a982e5ce26
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194

View File

@ -1079,6 +1079,8 @@ comment-token = "--"
block-comment-tokens = { start = "/-", end = "-/" }
language-servers = [ "lean" ]
indent = { tab-width = 2, unit = " " }
rulers = [101]
text-width = 100
[language.auto-pairs]
'(' = ')'