removed note about "IO exceptions" during HTML generation
authorclasohm
Tue, 27 Feb 1996 13:01:16 +0100
changeset 1520 5fee0fef5019
parent 1519 f999804f11ea
child 1521 4ed3004ff75e
removed note about "IO exceptions" during HTML generation (Isabelle now just prints a warning)
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