# HG changeset patch
# User clasohm
# Date 822656709 -3600
# Node ID ee54d2c15d6625df3b0af24272c329e405ebd3ce
# Parent  6803ecb9b198d3081fa078f5733bd0e18da07df8
added warning for databases made with set MAKE_HTML

diff -r 6803ecb9b198 -r ee54d2c15d66 doc-src/Ref/theories.tex
--- a/doc-src/Ref/theories.tex	Tue Jan 23 14:25:55 1996 +0100
+++ b/doc-src/Ref/theories.tex	Fri Jan 26 12:45:09 1996 +0100
@@ -484,6 +484,17 @@
 make
 \end{ttbox}
 
+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.
+
+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
+database.
+
 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
 should not make HTML files for a logic if the HTML files for the base