I updated the bug with a new comment. https://sourceware.org/bugzilla/show_bug.cgi?id=10311#c10 I fumbled the bugzilla interface and added the same comment twice, but don't see any way to delete one of them.