src/Pure/General/comment.ML
changeset 69968 1a400b14fd3a
parent 69966 cba5b866c633
child 70229 c03f381fd373
     1.1 --- a/src/Pure/General/comment.ML	Sun Mar 24 17:45:00 2019 +0100
     1.2 +++ b/src/Pure/General/comment.ML	Sun Mar 24 17:53:46 2019 +0100
     1.3 @@ -34,7 +34,7 @@
     1.4        markups = [Markup.language_text true, Markup.raw_text]}),
     1.5     (Latex,
     1.6       {symbol = Symbol.latex, blanks = false,
     1.7 -      markups = [Markup.language_latex true, Markup.no_words, Markup.raw_text]}),
     1.8 +      markups = [Markup.language_latex true, Markup.raw_text]}),
     1.9     (Marker,
    1.10       {symbol = Symbol.marker, blanks = false,
    1.11        markups = [Markup.language_document_marker]})];