# HG changeset patch
# User haftmann
# Date 1114754706 -7200
# Node ID dcce462301315d5f4182866297531d7c1ca9643e
# Parent  d6aa6c707acf81d2192cffde52695784ec3583f2
added antiquotations typeof, const, term_style, thm_style, term_type (something still to be done)

diff -r d6aa6c707acf -r dcce46230131 etc/settings
--- a/etc/settings	Fri Apr 29 08:03:01 2005 +0200
+++ b/etc/settings	Fri Apr 29 08:05:06 2005 +0200
@@ -60,7 +60,7 @@
 
 
 ###
-### Compilation options for isatool usedir[B
+### Compilation options for isatool usedir
 ### (as on command line)
 ###