Zulip Chat Archive

Stream: Zulip meta

Topic: quoting codeblocks


view this post on Zulip Kenny Lau (Aug 17 2020 at 13:47):

I can type codes without the closing backticks

view this post on Zulip Kenny Lau (Aug 17 2020 at 13:48):

Kenny Lau said:

I can type codes without the closing backticks
````
but if I reply to such a message, things go south

view this post on Zulip Kevin Buzzard (Aug 17 2020 at 13:50):

that'll teach you

view this post on Zulip Kenny Lau (Aug 17 2020 at 13:50):

so it's not a feature?

view this post on Zulip Kevin Buzzard (Aug 17 2020 at 13:51):

feel free to open an issue at Zulip :-) Hopefully they'll fix the code-without-closing-backtick bug

view this post on Zulip Kenny Lau (Aug 17 2020 at 13:52):

it wasn't a problem until we decided that backticks without any langugage specification means Lean

view this post on Zulip Kenny Lau (Aug 17 2020 at 13:52):

because if you type any language name and press shift+enter, you get the closing backticks automatically

view this post on Zulip Johan Commelin (Aug 17 2020 at 13:52):

That was one of the best decisions ever (-;

view this post on Zulip Kenny Lau (Aug 17 2020 at 13:52):

yeah but now the closing backticks aren't provided automatically

view this post on Zulip Kenny Lau (Aug 17 2020 at 13:53):

<--- so this lazy guy decided to train his muscle memory to not type the closing backticks

view this post on Zulip Kevin Buzzard (Aug 17 2020 at 13:53):

feel free to still put lean

view this post on Zulip Kenny Lau (Aug 17 2020 at 13:53):

<-- lazy

view this post on Zulip Johan Commelin (Aug 17 2020 at 13:53):

<-- muscle memory

view this post on Zulip Mario Carneiro (Aug 17 2020 at 15:30):

You must be one of the heathens who opens <p> tags and never closes them

view this post on Zulip Johan Commelin (Aug 17 2020 at 15:32):

/me shivers <br/> <br/> <br/>

view this post on Zulip Kevin Buzzard (Aug 17 2020 at 15:57):

I remember the days when opening <p> tags without closing them was legal

view this post on Zulip Mario Carneiro (Aug 17 2020 at 15:59):

or <html> and <body>

view this post on Zulip Gabriel Ebner (Aug 17 2020 at 16:01):

@Kevin Buzzard It's completely legal not to close <p> elements in (the current version of) HTML5: https://html.spec.whatwg.org/multipage/parsing.html#unclosed-formatting-elements
It is even defined what the following means:

<p><b>This is bold
<p>This is a different paragraph (not nested in the first one), but still bold!

view this post on Zulip Mario Carneiro (Aug 17 2020 at 16:05):

what, this is nuts

view this post on Zulip Mario Carneiro (Aug 17 2020 at 16:06):

this is what happens when you give in to peer pressure

view this post on Zulip Mario Carneiro (Aug 17 2020 at 16:06):

just say no to malformed HTML

view this post on Zulip Jalex Stark (Aug 17 2020 at 22:26):

I went to the Zulip zulip to ask a question about the linkifier and they were pretty friendly


Last updated: May 08 2021 at 23:10 UTC