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 <k...@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. >