author | wenzelm |
Tue, 31 Jul 2007 21:19:23 +0200 | |
changeset 24101 | bdcefe679ced |
parent 24100 | a2f19514e156 |
child 24102 | 969d334040a8 |
--- a/src/Pure/Thy/html.ML Tue Jul 31 21:19:22 2007 +0200 +++ b/src/Pure/Thy/html.ML Tue Jul 31 21:19:23 2007 +0200 @@ -305,7 +305,7 @@ (* document *) val charset = ref "iso-8859-1"; -fun with_charset s = setmp charset s; +fun with_charset s = setmp_noncritical charset s; fun begin_document title = "<!DOCTYPE HTML PUBLIC \"-//W3C//DTD HTML 4.01 Transitional//EN\" \