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.