Helmut Karlowski wrote:
using $(SHELL) instead of sh, little efficiency-improvement
This is good and cleaner.However, since make ignores the SHELL environment variable and always set it to /bin/sh, there will be no efficiency improvement.
http://www.gnu.org/software/make/manual/html_node/Choosing-the-Shell.html Of course one can do make SHELL=/bin/bash to override it explicitly. -- Vincent Rivière