Re: remove deprecated @@@ operator ?

On Sun, Oct 21, 2018 at 04:24:16PM -0400, Tom Lane wrote:
> 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 ...

Done in the attached patch.

-- 
  Bruce Momjian  <bruce@momjian.us>        https://momjian.us
  EDB                                      https://enterprisedb.com

  Only you can decide what is important to you.