# HG changeset patch # User wenzelm # Date 1185909563 -7200 # Node ID bdcefe679ced391feef714ea3d814d75fcafbf9e # Parent a2f19514e15614f3d2093dbb69e1bd0356d4a144 with_charset: setmp_noncritical; diff -r a2f19514e156 -r bdcefe679ced src/Pure/Thy/html.ML --- 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 = "