Okay, I think I fixed it -- minor error in my past bug fix. Try the new commit.
On Dec 31, 2016, at 9:07 AM, Sean Luke <[log in to unmask]> wrote:
>> (Sean, should I just send this kind of bug report directly to you, or is it best to send it to the mailing list?)
> At this rate, send 'em directly to me. The examples help a lot in nailing the bug fast.
> Remember that I'm in Italy with very limited internet access and a kinda slow turnaround.
> Though this one should be traceable fast.