> Do we want to introduce case-sensitive options? If nobody objects > strongly, I will make all current options case-sensitive-lowercase-required > and then we'll have a lot more options, so to speak. :-) > > I am in favor of making the options case-sensitive.