# HG changeset patch # User wenzelm # Date 1445879057 -3600 # Node ID 8e3705d91cfa18915b96cad73b15d48c5cefc424 # Parent c64628dbac00a422992d1c6e6c72374898ad7d08 clarified Latex.environment (again, amending e16649b70107): avoid additional paragraph, e.g. relevant for option [display]; diff -r c64628dbac00 -r 8e3705d91cfa 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\