# 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