It doesn't appear you've pushed your own initial patch, though...

--
Tim Parenti

On 9 October 2014 16:19, Paul Eggert <eggert@cs.ucla.edu> wrote:

Thanks, I pushed that into the experimental github version.