Robert Haas <robertmhaas@gmail.com> writes:
> On Tue, May 30, 2017 at 8:55 PM, David G. Johnston
> <david.g.johnston@gmail.com> wrote:
>>> Having --no-comments seems generally useful to me, in any case.
>> It smacks of being excessive to me.
> It sounds perfectly sensible to me. It's not exactly an elegant
> solution to the original problem, but it's a reasonable switch on its
> own merits.
I dunno. What's the actual use-case, other than as a bad workaround
to a problem we should fix a different way?
regards, tom lane