Merge pull request tock#504 from jrvanwhy/makefile-shell

Specify Bash as the shell to use in Makefile.
jrvanwhy · Aug 21, 2023 · 110af62 · 110af62
2 parents c2fef04 + e542dd2
commit 110af62
Showing 1 changed file with 4 additions and 0 deletions.
diff --git a/Makefile b/Makefile
@@ -1,3 +1,7 @@
+# Make uses /bin/sh by default, which is a different shell on different OSes.
+# Specify Bash instead so we don't have to test against a variety of shells.
+SHELL := /bin/bash
+
 # By default, let's print out some help
 .PHONY: usage
 usage: