author | wenzelm |
Sat, 13 Jan 2018 20:01:33 +0100 | |
changeset 67421 | c4a10621c72e |
parent 67420 | c4c8787ed669 |
child 67422 | eec44c98d8b3 |
--- a/src/Pure/Thy/thy_output.ML Sat Jan 13 19:50:37 2018 +0100 +++ b/src/Pure/Thy/thy_output.ML Sat Jan 13 20:01:33 2018 +0100 @@ -124,7 +124,7 @@ val source = Input.source true (Symbol_Pos.implode body) (Symbol_Pos.range body); in output_text ctxt {markdown = false} source - |> Latex.enclose_body "%\n\\isamarkupcmt{" "}" + |> Latex.enclose_body "%\n\\isamarkupcmt{" "%\n}" end); in