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