Re: remove deprecated @@@ operator ?

Oleg Bartunov <obartunov@postgrespro.ru> writes:
> The  commit 9b5c8d45f62bd3d243a40cc84deb93893f2f5122 is now 10+ years
> old, may be we could remove deprecated @@@ operator ?

Is it actually causing any problem?  AFAICS it's just a couple extra
pg_operator entries, so why not leave it?

I'd be +1 for removing it from the docs, though ...

            regards, tom lane