--- 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=""
###