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.

Thanks.