Oh, no no answer.  I had forgotten!  We can get this merged now and adopt a
better way if we find one.