I made the changes, updated the commit message for the large patch, and
pushed.

On Sat, Oct 24, 2020 at 10:40 PM Kyle Meyer <kyle@kyleam.com> wrote:

> ian martins writes:
>
> > After making the changes, should I submit updated patches or is it fine
> to
> > push?
>
> Push away.  Thanks again.
>