From a982e5ce260e8191a2a24fa62e9e5bdf488bb5d4 Mon Sep 17 00:00:00 2001 From: Ashley Vaughn <59515175+ashl3y-v@users.noreply.github.com> Date: Sat, 22 Jun 2024 18:09:39 -0700 Subject: [PATCH] add ruler at 101 and text-width at 100 to lean in languages.toml (#10969) --- languages.toml | 2 ++ 1 file changed, 2 insertions(+) diff --git a/languages.toml b/languages.toml index eff4ca0626ed..7ffc998b8a36 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] '(' = ')'