author | wenzelm |
Sun, 24 Mar 2019 17:19:30 +0100 | |
changeset 69963 | 396e0120f7b8 |
parent 69962 | 82e945d472d5 |
child 69964 | 699ffc7cbab8 |
--- 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