On Tue, Oct 16, 2018, at 4:33 PM, Helmut K. C. Tessarek wrote: > -----BEGIN PGP SIGNED MESSAGE----- > Hash: SHA512 > > I've changed the commit message as James suggested. > > Do I have to do anything else to get someone to commit it? I can push this in about a week unless someone else does first. Ping if I forget after 25 Oct.