# HG changeset patch # User wenzelm # Date 1218485211 -7200 # Node ID 992c6d9849254af3709190a4d1e0054062e36585 # Parent 20aea331137fb6d7dcfe89207c9f53ab6ef3dbd1 : more XHTML 1.0 Transitional conformance; diff -r 20aea331137f -r 992c6d984925 src/Pure/Thy/html.ML --- a/src/Pure/Thy/html.ML Mon Aug 11 22:06:49 2008 +0200 +++ b/src/Pure/Thy/html.ML Mon Aug 11 22:06:51 2008 +0200 @@ -333,8 +333,8 @@ "\n\n
\n
\n\ \\n\ - \\n\ + \width=" ^ quote width ^ " height=" ^ quote height ^ ">\n\ + \\n\ \\n
" ^ end_document) end; in map applet_page sizes end;