replaced ISABELLE_HTML by ISABELLE_USEDIR_OPTIONS;
authorwenzelm
Fri Apr 04 19:09:21 1997 +0200 (1997-04-04)
changeset 29154d2d409fe2ea
parent 2914 01d24f98528f
child 2916 d761a62da697
replaced ISABELLE_HTML by ISABELLE_USEDIR_OPTIONS;
etc/settings
     1.1 --- a/etc/settings	Fri Apr 04 19:08:35 1997 +0200
     1.2 +++ b/etc/settings	Fri Apr 04 19:09:21 1997 +0200
     1.3 @@ -39,11 +39,10 @@
     1.4  
     1.5  
     1.6  ###
     1.7 -### Compilation options
     1.8 +### Misc options
     1.9  ###
    1.10  
    1.11 -# HTML generation (should be 'true' or 'false').
    1.12 -ISABELLE_HTML=false
    1.13 +ISABELLE_USEDIR_OPTIONS=""
    1.14  
    1.15  
    1.16  ###