Thanks. Actually, it worked even without the <pre> tag (I think it's ok without monospace). Benoît
On Thursday, September 22, 2022 at 5:17:42 PM UTC+2 [email protected] wrote: > Did you try doubled backtick? That is, <pre> `` -> `` </pre> if you want > to display " ` -> ` " in monospace. > > On Thu, Sep 22, 2022 at 11:06 AM Benoit <[email protected]> wrote: > >> I am trying to display a backquote in a comment with an <HTML> tag. >> >> The failed attempt appears on >> https://us.metamath.org/mpeuni/conventions-comments.html where I wanted >> to display: >> >> ...use embedded mathematical symbols when they have been defined (e.g.,` >> -> ` for [the displayed symbol \rightarrow]) >> >> I tried using <pre> ` -> ` </pre> but obviously it didn't work... >> >> (Rk: unrelated, but there is a typo "source source" in that page which >> has been fixed in a PR) >> >> Thanks for your help, >> Benoît >> >> -- >> You received this message because you are subscribed to the Google Groups >> "Metamath" group. >> To unsubscribe from this group and stop receiving emails from it, send an >> email to [email protected]. >> To view this discussion on the web visit >> https://groups.google.com/d/msgid/metamath/e8b66d1f-f4ed-4606-a6c2-50aa8ef68570n%40googlegroups.com >> >> <https://groups.google.com/d/msgid/metamath/e8b66d1f-f4ed-4606-a6c2-50aa8ef68570n%40googlegroups.com?utm_medium=email&utm_source=footer> >> . >> > -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/c2411b6e-2229-484d-860d-fcd9985090a2n%40googlegroups.com.
