On Sat, Oct 28, 2017 at 10:00 PM, Shiro Kawai <xxxxxx@gmail.com> wrote:
The changes in #1 is already hand-merged by John (commit 3199d22). PR #2 is created on top of master HEAD and unrelated to #1. Sorry for the confusion.
Oh, I see. I was confused because your change to the description of gmap, which John approved separately in principle, wasn't included in #2, so I assumed that the rest was also important.
Would you mind sending me a pull request for that? I prefer to have fixes like that submitted by authors rather than applied manually by me.