| changeset 61462 | e16649b70107 |
| parent 61457 | 3e21699bb83b |
| child 61473 | 34d1913f0b20 |
--- a/src/Pure/Tools/rail.ML Sat Oct 17 19:47:34 2015 +0200 +++ b/src/Pure/Tools/rail.ML Sat Oct 17 20:27:12 2015 +0200 @@ -354,11 +354,7 @@ output "" rail' ^ "\\rail@end\n" end; - in - "\\begin{railoutput}\n" ^ - implode (map output_rule rules) ^ - "\\end{railoutput}\n" - end; + in Latex.environment "railoutput" (implode (map output_rule rules)) end; in