Joseph Myers, le mer. 31 oct. 2018 02:13:54 +0000, a ecrit: > Also, shouldn't there be a regeneration of errno.texi?
Mmm, actually that was the contrary. And the script to regenerate these was emitting an absolute path. I have now fixed these and regenerated every errno things. It seems at push time I introduced spurious merge commits, I probably missed a rebased to avoid it, sorry about that. Samuel
