# HG changeset patch
# User clasohm
# Date 822660216 -3600
# Node ID a4896058a47e4857d6be24e9662854b14d9f5728
# Parent  ee54d2c15d6625df3b0af24272c329e405ebd3ce
extended warning regarding MAKE_HTML databases

diff -r ee54d2c15d66 -r a4896058a47e doc-src/Ref/theories.tex
--- a/doc-src/Ref/theories.tex	Fri Jan 26 12:45:09 1996 +0100
+++ b/doc-src/Ref/theories.tex	Fri Jan 26 13:43:36 1996 +0100
@@ -486,13 +486,18 @@
 
 When using ML databases made this way to load additional theories or
 derive other databases from them, you have to be aware that HTML
-generation remains activated.
+generation remains activated. Also be especially 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.
 
 The reason is that the boolean reference variable {\tt make_html} (see
 below) is set. Therefore HTML files are generated unless you assign a
-value of {\tt false} to {\tt make_html}. The only place where the
-environment variable {\tt MAKE_HTML} is used is in the makefile where
-it determines the initial value of {\tt make_html} for a newly made
+value of {\tt false} to {\tt make_html}.
+
+This is not influenced by the environment variable {\tt MAKE_HTML},
+because the only place where it is used is in the makefile where it
+determines the initial value of {\tt make_html} for a newly made
 database.
 
 As some of Isabelle's logics are based on others (e.g. {\tt ZF} on