Nov. 9, 2015
4:01 p.m.
Thanks for the heads-up. Proposed patch attached. We'll need a new release of course, but this does not seem to be urgent.