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.