diff -r a24865b6262f -r 9efccbad7d42 src/Pure/Thy/html.scala --- a/src/Pure/Thy/html.scala Wed Feb 13 11:25:23 2019 +0100 +++ b/src/Pure/Thy/html.scala Thu Feb 14 14:44:41 2019 +0100 @@ -324,8 +324,8 @@ /* document */ val header: String = - """ - + XML.header + + """ """ val head_meta: XML.Elem =