merge 21766 21769
quit

Yes, the bug was just filed as #21766 and we're working on it.

Thanks for your test case, which is *much* shorter than the one in bug#21766.