Enumerations are rendered incorrectly in doc. comments

JetBrains / intellij-arend

Arend plugin for IntelliJ IDEA

Apache License 2.0

90 stars 12 forks source link

Open sxhya opened 1 month ago

sxhya commented 1 month ago

In this example leading "-"'s are part of doc. comment syntax.

The example can be found in arend-lib/master

sxhya commented 1 month ago

Also I don't like colors of links in doc. comments (they do not work well for all color schemes).

sxhya commented 1 month ago

Also the problem is that list labels are duplicated (both in standard and alternative browser)