etc/settings
changeset 15881 dcce46230131
parent 15880 d6aa6c707acf
child 15982 9d7f3db40b88
--- 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)
 ###