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.)