On Thu, Jan 24, 2019 at 08:56:05AM -0300, Alvaro Herrera wrote:
> Uh, I didn't think it was necessary nor desirable to rename the flag,
> only the user-visible message.
Oh, OK. I have overstated your comment then. Are you fine with the
attached instead? The flag name remains the same, and the comment is
updated.
--
Michael