From e542dd2294ccf40e954cce53c6a0feab8c75eecd Mon Sep 17 00:00:00 2001
From: Johnathan Van Why <jrvanwhy@google.com>
Date: Tue, 15 Aug 2023 10:54:13 -0700
Subject: [PATCH] Specify Bash as the shell to use in Makefile.

Closes #502.
---
 Makefile | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/Makefile b/Makefile
index 7b6cc2db..48c58f53 100644
--- 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: