Re: [PATCH v2] Makefile: set default goals in makefiles

> Explicitly set the default goal at the very top of various makefiles.
> This is already present in some makefiles, but not all of them.
> 
> In particular, this corrects a regression introduced in a38edab7c8
> (Makefile: generate doc versions via GIT-VERSION-GEN, 2024-12-06).  That
> commit added some config files as build targets for the Documentation
> directory, and put the target configuration in a sensible place.
> Unfortunately, that sensible place was above any other build target
> definitions, meaning the default goal changed to being those
> configuration files only, rather than the HTML and man page
> documentation.