It's not documented because the details are complex and hard to
explain, and the result isn't supposed to depend on whether Make
invokes commands directly or via the shell. So why do you care to
know which way does make invoke a given command?
Not so complex and hard to explain that you couldn't concisely explain it in this thread and [that thread](
https://lists.gnu.org/archive/html/make-w32/2020-05/msg00001.html). Just use one of the two explanations you gave. They're totally sufficient, in my opinion. The manual for Make is tens of thousands of words long and explains a few much more complicated ideas. This addition wouldn't look out of place in the least.
> GNU Make doesn't invoke the shell unless it (a) sees a shell
built-in command, or (b) sees some character special to the
shell. Since the built-in commands of PowerShell are not known to
GNU Make, you are left with the second option, and the no-op
redirection achieves that.
> To trigger the use of a shell, you need to use some feature on the
command line that needs a shell. For example, redirection or some
fancy quoting.
What for? Make is for building programs by running shell commands.
As long as the results of running a command are the same, why should
you care how that command is invoked, and why would you need a way to
force invocation via the shell?
You assume that the results are the same. This thread and that thread have demonstrated that they are not. I'm less offended that the shell isn't invoked than I am that it is not documented _why_ it isn't invoked. I had a Makefile that I thought should work according to the documented behavior, and it didn't. _That_ is why I care how the commands are invoked. My commands work in the shell, and don't work without the shell. So please let me use the shell without having to sign up for the mailing list and jump through an extra hoop on every command. A naive implementation would do the right thing every time. This optimization is doing the wrong thing some of the time.