# HG changeset patch
# User webertj
# Date 1056968580 -7200
# Node ID aed5d25c4a0cbd4b2a7a36ed189b0efa4738d3f6
# Parent c69d5bf3047d2fb30b50305ac2aaf067a0531b2b
Added DOCTYPE and Content-type to HTML documents.
diff -r c69d5bf3047d -r aed5d25c4a0c src/Pure/Thy/html.ML
--- a/src/Pure/Thy/html.ML Sun Jun 29 21:29:15 2003 +0200
+++ b/src/Pure/Thy/html.ML Mon Jun 30 12:23:00 2003 +0200
@@ -164,8 +164,11 @@
(* document *)
fun begin_document title =
- "\n\
+ "\n\
+ \\n\
+ \\n\
\\n\
+ \\n\
\" ^ plain (title ^ " (" ^ version ^ ")") ^ "\n\
\\n\
\\n\