Subject: done

From: Tom Tromey <[email-masked]>
Date: Sat, 11 Aug 2018 18:24:07 -0600

The fix to this was checked in a while ago.

Tom