clarified Latex.environment (again, amending e16649b70107): avoid additional paragraph, e.g. relevant for option [display];
authorwenzelm
Mon, 26 Oct 2015 18:04:17 +0100
changeset 61516 8e3705d91cfa
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
--- a/src/Pure/Thy/latex.ML	Sun Oct 25 17:31:14 2015 +0100
+++ b/src/Pure/Thy/latex.ML	Mon Oct 26 18:04:17 2015 +0100
@@ -159,7 +159,7 @@
 (* theory presentation *)
 
 fun environment name =
-  enclose ("%\n\\begin{" ^ name ^ "}%\n") ("%\n\\end{" ^ name ^ "}%\n");
+  enclose ("%\n\\begin{" ^ name ^ "}%\n") ("%\n\\end{" ^ name ^ "}");
 
 val tex_trailer =
   "%%% Local Variables:\n\