# HG changeset patch
# User wenzelm
# Date 1390075434 -3600
# Node ID 368ee97e03ce5033fa1cf2d2de9e77989cc073b7
# Parent  eb3c9b457cb0ad700c37c7660080732ebe2e6b95
HTML output for \<newline>;

diff -r eb3c9b457cb0 -r 368ee97e03ce src/Pure/Thy/html.ML
--- a/src/Pure/Thy/html.ML	Sat Jan 18 20:51:48 2014 +0100
+++ b/src/Pure/Thy/html.ML	Sat Jan 18 21:03:54 2014 +0100
@@ -190,6 +190,7 @@
     ("\\<rightarrow>", (2, "-&gt;")),
     ("\\<open>", (1, "&#8249;")),
     ("\\<close>", (1, "&#8250;")),
+    ("\\<newline>", (1, "&#9166;")),
     ("\\<^bsub>", (0, hidden "&#8664;" ^ "<sub>")),
     ("\\<^esub>", (0, hidden "&#8665;" ^ "</sub>")),
     ("\\<^bsup>", (0, hidden "&#8663;" ^ "<sup>")),