extended warning regarding MAKE_HTML databases
authorclasohm
Fri Jan 26 13:43:36 1996 +0100 (1996-01-26)
changeset 1453a4896058a47e
parent 1452 ee54d2c15d66
child 1454 d0266c81a85e
extended warning regarding MAKE_HTML databases
doc-src/Ref/theories.tex
     1.1 --- a/doc-src/Ref/theories.tex	Fri Jan 26 12:45:09 1996 +0100
     1.2 +++ b/doc-src/Ref/theories.tex	Fri Jan 26 13:43:36 1996 +0100
     1.3 @@ -486,13 +486,18 @@
     1.4  
     1.5  When using ML databases made this way to load additional theories or
     1.6  derive other databases from them, you have to be aware that HTML
     1.7 -generation remains activated.
     1.8 +generation remains activated. Also be especially careful when making
     1.9 +such databases publicly available since it means that your users might
    1.10 +get into trouble that they don't expect, like IO exceptions caused by
    1.11 +insufficient write access.
    1.12  
    1.13  The reason is that the boolean reference variable {\tt make_html} (see
    1.14  below) is set. Therefore HTML files are generated unless you assign a
    1.15 -value of {\tt false} to {\tt make_html}. The only place where the
    1.16 -environment variable {\tt MAKE_HTML} is used is in the makefile where
    1.17 -it determines the initial value of {\tt make_html} for a newly made
    1.18 +value of {\tt false} to {\tt make_html}.
    1.19 +
    1.20 +This is not influenced by the environment variable {\tt MAKE_HTML},
    1.21 +because the only place where it is used is in the makefile where it
    1.22 +determines the initial value of {\tt make_html} for a newly made
    1.23  database.
    1.24  
    1.25  As some of Isabelle's logics are based on others (e.g. {\tt ZF} on