I thought of this, but exactly where on the site I would post this one was unclear to me. In any case, I believe (from a /msg I got) that approximately this bug has been posted previously to the MySQL developers list, which seems a more appropriate place for it—I'm not sure that putting a comment on the doc pages would be much more helpful. On the other hand, it could at least provide some comfort to the next schlub to be caught by this...