I've just pushed four commits, including the two attached here.
I've elided the gnulib-update and copyright-update ones as too large
and all mechanical.