added antiquotations typeof, const, term_style, thm_style, term_type (something still to be done)
authorhaftmann
Fri Apr 29 08:05:06 2005 +0200 (2005-04-29)
changeset 15881dcce46230131
parent 15880 d6aa6c707acf
child 15882 a191d2bee3e1
added antiquotations typeof, const, term_style, thm_style, term_type (something still to be done)
etc/settings
     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