Subject: done
From: Tom Tromey <[email-masked]>
To: [email-masked]
Date: Sat, 11 Aug 2018 18:24:07 -0600
List-Id: <debbugs-submit.debbugs.gnu.org>

The fix to this was checked in a while ago.

Tom