Zulip Chat Archive

Stream: Lean Together 2019

Topic: comments highlighting

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Jul 09 2020 at 23:11):

@Patrick Massot Is this maybe in the wrong stream?

view this post on Zulip Notification Bot (Jul 10 2020 at 00:05):

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

Last updated: May 08 2021 at 21:09 UTC