# HG changeset patch
# User wenzelm
# Date 860173761 -7200
# Node ID 4d2d409fe2ea18eed9d120cbb9617e36d4b00634
# Parent  01d24f98528f61491d69da21b1402488d9b02eeb
replaced ISABELLE_HTML by ISABELLE_USEDIR_OPTIONS;

diff -r 01d24f98528f -r 4d2d409fe2ea etc/settings
--- a/etc/settings	Fri Apr 04 19:08:35 1997 +0200
+++ b/etc/settings	Fri Apr 04 19:09:21 1997 +0200
@@ -39,11 +39,10 @@
 
 
 ###
-### Compilation options
+### Misc options
 ###
 
-# HTML generation (should be 'true' or 'false').
-ISABELLE_HTML=false
+ISABELLE_USEDIR_OPTIONS=""
 
 
 ###