On 03/31/2015 07:06 AM, Richard Stallman wrote:
> there's no real issue here.
Thanks for looking into it.  I installed the attached patch, which is 
essentially Pete's patch but with minor sorting and suchlike changes.  I 
marked it as "tiny change" as it's small enough that we needn't worry 
about copyright papers.