Unnamed repository; edit this file 'description' to name the repository.
add ruler at 101 and text-width at 100 to lean in languages.toml (#10969)
| -rw-r--r-- | languages.toml | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/languages.toml b/languages.toml index eff4ca06..7ffc998b 100644 --- a/languages.toml +++ b/languages.toml @@ -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] '(' = ')' |