On Wed, 2018-05-16 at 11:52 +0200, Christophe de Dinechin wrote: > > > > > > save_errno as proposed or err_no ? > > :-) [Note to Jonathon: wouldn't this be read as "err… no!" ???] > No, not really ;) I don't really feel strongly about any of the options here. Jonathon