Subject: bug#15066: ./configure && make && make install

From: Paul Eggert <[email-masked]>
Date: Sat, 10 Aug 2013 08:13:19 -0700

On 08/10/2013 06:57 AM, Bernhard Voelker wrote:
> if you want the want to have it changed, please report this
> issue there.

No need; I fixed it upstream just now.  Thanks for reporting the problem.