| changeset 62529 | 8b7bdfc09f3b |
| parent 61595 | 3591274c607e |
| child 62804 | 7b9c5416f30e |
--- a/src/Pure/Thy/markdown.ML Sun Mar 06 13:19:19 2016 +0100 +++ b/src/Pure/Thy/markdown.ML Sun Mar 06 16:19:02 2016 +0100 @@ -49,7 +49,7 @@ val kinds = [("item", Itemize), ("enum", Enumerate), ("descr", Description)]; -val is_control = member (op =) ["\\<^item>", "\\<^enum>", "\\<^descr>"]; +val is_control = member (op =) ["\<^item>", "\<^enum>", "\<^descr>"]; (* document lines *)