Christopher Genovese <genovese@cmu.edu> writes:
> Do you want me to submit a new patch with these changes?
It would be useful. Someone other than me may try this patch
without reading all the bug report, and repeat some of my comments.
Once we update the patch we can wait like 1 week; if we don't
get further comments after that week, then it's OK for me to push
the fix to master branch.
Thank you