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.