SHELL has been explicitly set to /bin/bash

On some systems, the default shell `/bin/sh' doesn't point to Bash and
this can cause problems and failures when the designer uses its
features. Bash (and its extra features) make things very easy and it
is very ubiquitous, so it is safe to assume users will have it.

This problem was reported by Alejandro Serrano Borlaff.

1 files changed, 13 insertions, 0 deletions

diff --git a/Makefile b/Makefile
index f63c5d6..3bbafcd 100644
--- a/Makefile
+++ b/Makefile
@@ -41,6 +41,19 @@ all: reproduce/build paper.pdf
 
 
 
+# Use Bash as the shell
+# ---------------------
+#
+# Some systems don't default to Bash as the shell they use to execute
+# the recipes or run Make's `$(shell)' function. So to be sure the
+# scripts are executed in a similar manner on all systems, we'll set
+# the default shell for this pipeline to be Bash.
+SHELL := /bin/bash
+
+
+
+
+
 # Include specific Makefiles
 # --------------------------
 #