> I propose it
> should be case insensitive -- it would be very confusing to have two
> classes whose names differed only by case. Any objections from
> anyone?
Fine with me. The next question is which case will be shown in the
displays, in case of a conflict. Use the one in models.wrm in preference
to options.wrm or other, code-installed versions?
- Dave