Subject: 13880 is done

From: Paul Eggert <[email-masked]>
Date: Tue, 12 Mar 2013 13:47:30 -0700

close 13880
thanks

I fixed this but forgot to mark it as done.