# HG changeset patch # User wenzelm # Date 1218812636 -7200 # Node ID 220e7a18a8ea1411b0b5a078bc9775ead5720cd1 # Parent e4f8763b971b1bbcaf9b5eb644afbf3adce5a614 fixed DOCTYPE -- XHTML is case-sensitive! diff -r e4f8763b971b -r 220e7a18a8ea src/Pure/Thy/html.ML --- a/src/Pure/Thy/html.ML Fri Aug 15 17:03:55 2008 +0200 +++ b/src/Pure/Thy/html.ML Fri Aug 15 17:03:56 2008 +0200 @@ -274,7 +274,7 @@ fun begin_document title = let val cs = ! charset in "\n\ - \\n\ \\n\ \\n\