# HG changeset patch
# User clasohm
# Date 825422476 -3600
# Node ID 5fee0fef5019f3a48510a91a241a23ab3efce3d7
# Parent  f999804f11eaf5a9eff74a6c6383af4bd391ffa4
removed note about "IO exceptions" during HTML generation
(Isabelle now just prints a warning)

diff -r f999804f11ea -r 5fee0fef5019 doc-src/Ref/theories.tex
--- a/doc-src/Ref/theories.tex	Thu Feb 22 18:35:16 1996 +0100
+++ b/doc-src/Ref/theories.tex	Tue Feb 27 13:01:16 1996 +0100
@@ -504,9 +504,8 @@
 databases derived from it will now cause HTML files to be written.
 This behaviour can be changed by assigning a value of {\tt false} to
 the boolean reference variable {\tt make_html}. Be careful when making
-such databases publicly available since it means that your users might
-get into trouble that they don't expect, like IO exceptions caused by
-insufficient write access.
+such databases publicly available since it means that your users will
+generate HTML files though they might not intend to do so.
 
 As some of Isabelle's logics are based on others (e.g. {\tt ZF} on
 {\tt FOL}) and because the HTML files list a theory's ancestors, you