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