>> undocumented. Maybe instead of removing, change the text to be >> "Deprecated, use the equivalent XXX operator instead." Or we could >> add a footnote similar to what was there for a previous renaming:
> The problem that this new <<| is equivalent to <^ only for points (To > recap: the source of a problem is the same name of <^ operator for points > and boxes with different meaning for these types).
I don't think it's that hard to be clear; see proposed wording below.
The other loose end is that I don't think we can take away the opclass entries for the old spellings, unless we're willing to visibly break people's queries by removing those operator names altogether. That doesn't seem like it'll fly when we haven't even deprecated the old names yet. So for now, we have to support both names in the opclasses. I extended the patch to do that.
This version seems committable to me --- any thoughts?
The wording seems no problem to me. I looked into a patch and changes also seem sensible but I can not apply this patch because of really many rejects. Which commit should I use to apply it onto?
