On Fri, Oct 13, 2017 at 07:07:56AM +0100, Christopher Baines wrote: > On Mon, 04 Sep 2017 15:09:48 +0200 > ludo@gnu.org (Ludovic Courtès) wrote: > > > Hey Leo, > > > > Leo Famulari skribis: > > > > > I *think* this patch is correct. I'm currently trying to get started > > > with Cuirass and this tripped me up. > > > > > > * doc/cuirass.texi (Specifications): Mention "name". > > > > I think you’re right, please push! > > Bump. Is this still ready to be merged, as I don't think it has been > merged yet? Sure, but I can't figure out how to push to this repo. What is the push URL?