Subject: fixed since commit 17e56dac1
From: Thomas Danckaert <[email-masked]>
To: [email-masked], [email-masked]
Date: Wed, 27 Sep 2017 09:39:23 +0200 (CEST)
List-Id: <debbugs-submit.debbugs.gnu.org>

Hi,

I think this one's fixed by now.  I wasn't aware of this bug report.

cheers,

Thomas