> Well, of course it can't be changed, but if Tim of all people made that
> mistake, I think it's a good indicator that something's wrong.
Na, I make a lot of mistakes at these ungodly early hours. "str1 in str2"
is the right solution now.