changeset 33222 | 89ced80833ac |
parent 32796 | 2e4485b9a39f |
child 33983 | cfbf1ff6170d |
--- a/src/Pure/Thy/html.ML Tue Oct 27 13:15:04 2009 +0100 +++ b/src/Pure/Thy/html.ML Tue Oct 27 13:15:20 2009 +0100 @@ -267,7 +267,7 @@ (* document *) val charset = Unsynchronized.ref "ISO-8859-1"; -fun with_charset s = setmp_noncritical charset s; (* FIXME *) +fun with_charset s = setmp_noncritical charset s; (* FIXME unreliable *) fun begin_document title = let val cs = ! charset in