Re: How to choose the shell?

[Eli Zaretskii]

> From: Paul Smith <psmith@gnu.org>
> Cc: make-w32@gnu.org
> Date: Sun, 05 Sep 2021 12:42:37 -0400
> 
> If you change the default shell, then make will never use any shortcuts
> since, obviously, it can't know what the syntax is of some other random
> shell.

I don't think Make on Windows does this bit.