Subject: bug#6806: checked in the patch

From: Tom Tromey <[email-masked]>
Date: Sat, 04 Feb 2017 13:29:11 -0700

I went ahead and checked in the patch, mostly because comment #20 said
it was fine, and also because it fixed a bug.

I think this bug should be left open, though, due to the other issues
identified.

Tom