I did 'make extraclean && . ../config-debug.sh && make' (all in one, to
ensure I didn't forget to clean) and it succeeded.

>
> I'm sorry I didn't look at this closer before, and thus caused you to
> work on all those changes, which we might now need to revert.

Yes, that's how hindsight works, you only get it when it's too late. ;)