add 100th line on lean web

Stream: mathlib4

[Kenny Lau]

Is there a way to add the ruler for the 100th column on lean web?

[Aaron Liu]

I would like to have this too
screenshot from VSCode so you can see it in action:
image.png

[Damiano Testa]

I would also like to have at least the option of displaying the ruler. As a partial workaround, you can set the linter option that checks for line length and at least get a warning on long lines:

import Mathlib.Tactic.Linter.Style
set_option linter.style.longLine true
/-
0123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890123456789
01234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890
-/