Set SHELL = /bin/dash only if it exists

src/test/run-make-fulldeps/tools.mk

@@ -21,11 +21,18 @@ CGREP := "$(S)/src/etc/cat-and-grep.sh"
 # diff with common flags for multi-platform diffs against text output
 DIFF := diff -u --strip-trailing-cr
 
-# CI platforms use `/bin/dash`. When compiling in other environments, the
-# default may be different (for example, may default to `/bin/bash`), and syntax
-# and results could be different. Ensure Makefile `$(shell ...)` invocations
-# always run in `dash`.
+# Some of the Rust CI platforms use `/bin/dash` to run `shell` script in
+# Makefiles. Other platforms, including many developer platforms, default to
+# `/bin/bash`. (In many cases, `make` is actually using `/bin/sh`, but `sh`
+# is configured to execute one or the other shell binary). `dash` features
+# support only a small subset of `bash` features, so `dash` can be thought of as
+# the lowest common denominator, and tests should be validated against `dash`
+# whenever possible. Most developer platforms include `/bin/dash`, but to ensure
+# tests still work when `/bin/dash`, if not available, this `SHELL` override is
+# conditional:
+ifneq (,$(wildcard /bin/dash))
 SHELL := /bin/dash
+endif
 
 # This is the name of the binary we will generate and run; use this
 # e.g. for `$(CC) -o $(RUN_BINFILE)`.