@cory Another aspect of this 'separate repo' thing is that every time you push a commit, resources are spent to run the tests--and they routinely fail, and I get email telling me that something's wrong...

@inducer I'm sorry about this - I'll make a separate repo. FWIW, the tests that were failing were due to the bug I found, but that's fixed now. Making a new repo is a good idea for the reasons you've stated elsewhere.

Np. Thanks for agreeing to do it.