> though that is probably inadequate.

Especially because Makefile.in is automatically generated. :-)

> It's not the default goal that matters, but if bootstrap4 is a goal at all.
> Or if compare3 is a goal.

I have a (correct) patch which I'll apply in a day or two.

Thanks,

Paolo

Reply via email to