Sorry, the patch still had bugs.  I fixed them.  I confirmed that the
patched version passed all regression tests.