# HG changeset patch
# User wenzelm
# Date 1553444370 -3600
# Node ID 396e0120f7b84415d9869895b795f7b0843d525c
# Parent  82e945d472d58f8385808eb2ca7164b371b5f693
clarified rendering: use COMMENT4 elsewhere;

diff -r 82e945d472d5 -r 396e0120f7b8 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