clarified rendering: use COMMENT4 elsewhere;
authorwenzelm
Sun, 24 Mar 2019 17:19:30 +0100
changeset 69963 396e0120f7b8
parent 69962 82e945d472d5
child 69964 699ffc7cbab8
clarified rendering: use COMMENT4 elsewhere;
src/Tools/jEdit/src/jedit_rendering.scala
--- a/src/Tools/jEdit/src/jedit_rendering.scala	Sun Mar 24 13:48:46 2019 +0100
+++ b/src/Tools/jEdit/src/jedit_rendering.scala	Sun Mar 24 17:19:30 2019 +0100
@@ -59,7 +59,7 @@
       Token.Kind.STRING -> LITERAL1,
       Token.Kind.ALT_STRING -> LITERAL2,
       Token.Kind.VERBATIM -> COMMENT3,
-      Token.Kind.CARTOUCHE -> COMMENT4,
+      Token.Kind.CARTOUCHE -> COMMENT3,
       Token.Kind.INFORMAL_COMMENT -> COMMENT1,
       Token.Kind.FORMAL_COMMENT -> COMMENT1,
       Token.Kind.ERROR -> INVALID