> 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