# HG changeset patch
# User wenzelm
# Date 1218485211 -7200
# Node ID 992c6d9849254af3709190a4d1e0054062e36585
# Parent  20aea331137fb6d7dcfe89207c9f53ab6ef3dbd1
<applet>: 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</div>\n<hr/>\n<div class=\"graphbrowser\">\n\
           \<applet code=\"GraphBrowser/GraphBrowser.class\" \
           \archive=\"GraphBrowser.jar\" \
-          \width=" ^ width ^ " height=" ^ height ^ ">\n\
-          \<param name=\"graphfile\" value=\"" ^ "session.graph" ^ "\">\n\
+          \width=" ^ quote width ^ " height=" ^ quote height ^ ">\n\
+          \<param name=\"graphfile\" value=\"" ^ "session.graph" ^ "\"/>\n\
           \</applet>\n<hr/>" ^ end_document)
       end;
   in map applet_page sizes end;