A note on code authorship — I pushed to this repo with old credentials (and a since-abandoned username rookie1024). The old commits are visible under the old-username branch but GitHub has decided to attribute them to a different user who took my previous name.