added antiquotations typeof, const, term_style, thm_style, term_type (something still to be done)
1.1 --- a/etc/settings Fri Apr 29 08:03:01 2005 +0200
1.2 +++ b/etc/settings Fri Apr 29 08:05:06 2005 +0200
1.3 @@ -60,7 +60,7 @@
1.4
1.5
1.6 ###
1.7 -### Compilation options for isatool usedir[B
1.8 +### Compilation options for isatool usedir
1.9 ### (as on command line)
1.10 ###
1.11