Subject: Re: typos

From: Noah Misch <[email-masked]>
Date: Tue, 5 Jul 2022 00:51:39 -0700

On Thu, Apr 14, 2022 at 08:56:22AM +1200, David Rowley wrote:
> 0007: Not pushed. No space after comment and closing */  pgindent
> fixed one of these but not the other 2.  I've not looked into why
> pgindent does 1 and not the other 2.

> -/* get operation priority  by its code*/
> +/* get operation priority by its code */

pgindent never touches comments that start in column zero.  (That's why many
column-0 comments are wrapped to widths other than the standard 78.)