clarified Latex.environment (again, amending e16649b70107): avoid additional paragraph, e.g. relevant for option [display];
authorwenzelm
Mon Oct 26 18:04:17 2015 +0100 (2015-10-26)
changeset 615168e3705d91cfa
parent 61515 c64628dbac00
child 61517 6cf5215afe8c
clarified Latex.environment (again, amending e16649b70107): avoid additional paragraph, e.g. relevant for option [display];
src/Pure/Thy/latex.ML
     1.1 --- a/src/Pure/Thy/latex.ML	Sun Oct 25 17:31:14 2015 +0100
     1.2 +++ b/src/Pure/Thy/latex.ML	Mon Oct 26 18:04:17 2015 +0100
     1.3 @@ -159,7 +159,7 @@
     1.4  (* theory presentation *)
     1.5  
     1.6  fun environment name =
     1.7 -  enclose ("%\n\\begin{" ^ name ^ "}%\n") ("%\n\\end{" ^ name ^ "}%\n");
     1.8 +  enclose ("%\n\\begin{" ^ name ^ "}%\n") ("%\n\\end{" ^ name ^ "}");
     1.9  
    1.10  val tex_trailer =
    1.11    "%%% Local Variables:\n\