Zulip Chat Archive

Stream: general

Topic: Markdown rendering issue in list.after


view this post on Zulip Eric Wieser (Dec 18 2020 at 09:34):

Any idea of the cause? docs#list.after. The word lean seems to have leaked out of ```lean ```

view this post on Zulip Gabriel Ebner (Dec 18 2020 at 09:36):

Maybe because there are spaces in front of the ```lean ?

view this post on Zulip Floris van Doorn (Dec 18 2020 at 18:13):

Here is a previous topic on this:
https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Documentation.20formatting.20in.20tactic.2Elocalized
It was not clear what causes this exactly. Indentation was a guess back then too, but there were some indented code blocks that did work correctly.


Last updated: May 12 2021 at 04:19 UTC