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: May 08 2021 at 21:09 UTC