Peter Geoghegan <pg@bowt.ie> writes:
> On Thu, Mar 18, 2021 at 4:40 PM Tom Lane <tgl@sss.pgh.pa.us> wrote:
>> Good question. We don't have a standard about that (whether to
>> do those in separate or the same commits), but we could establish one
>> if it seems helpful.
> I don't think that it matters too much, but it will necessitate
> updating the file multiple times. It might become natural to just do
> everything together in a way that it wasn't before.
Doubt that it matters. The workflow would have to be "commit and push
the mechanical updates, then edit the tracking file, commit and push
that". You don't have the commit hash nailed down till you've pushed.
So if we decided to do the mechanical updates in several commits,
not just one, I'd still be inclined to do them all and then edit the
tracking file once.
regards, tom lane