Rob Lewis

> > I thought MathJax was smart enough to do this, it handles ` > Do you have a docstring in mind that proves this? https://leanprover-community.github.io/mathlib_docs_demo/model_theory/order.html#first_order.language.sentence.densely_ordered is an example.

Even weirder, https://leanprover-community.github.io/mathlib_docs_demo/model_theory/order.html#first_order.language.term.realize_lt has both a working and broken occurence of `

I thought I just posted this (eaten by GitHub somehow?), but, the problem is `

#deploy

#deploy

[`6c05dba`](https://github.com/leanprover-community/doc-gen/pull/168/commits/6c05dba9f69da42cc6e3a85385c71ff1f24d2977) is clearly a hack, but I think it should work until the markdown/mathjax interaction is fixed. (Hypothesis: the informal text will never have a `

#deploy

#deploy

(the runners are backed up, the deploy may take a bit)

> I reckon this is ready to merge once @zhangir-azerbayev has fixed truncated translations? I've seen very few truncated translations, and regenerating the translations is costly. I think it's fine...