Zulip Chat Archive

Stream: Lean Together 2019

Topic: comments highlighting

Patrick Massot (Jul 09 2020 at 21:57):

In the VSCode extension, docstrings get some syntax highlighting, at least for stuff between backticks. Is there any obstacle to getting the same thing in comments?

Mario Carneiro (Jul 09 2020 at 23:11):

@Patrick Massot Is this maybe in the wrong stream?

Notification Bot (Jul 10 2020 at 00:05):

This topic was moved by Mario Carneiro to #general > comments highlighting

Last updated: Dec 20 2023 at 11:08 UTC