Paul Eggert Tue, 04 Sep 2012 13:58:56 -0700
Thanks. I think that's a known issue. It's not much of a problem in practice so I wouldn't worry about it.