aboutsummaryrefslogtreecommitdiff
path: root/Makefile
diff options
context:
space:
mode:
authorMohammad Akhlaghi <mohammad@akhlaghi.org>2018-07-27 12:50:19 +0200
committerMohammad Akhlaghi <mohammad@akhlaghi.org>2018-07-27 12:50:19 +0200
commitf41557ad13796424692ecca525b58fd03fc9dc7a (patch)
tree870618127304b65799e54aa2e45a07398774bfe2 /Makefile
parenta136e58c5d9a14ea09a13818201848ef98e9c5f9 (diff)
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.
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile13
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
# --------------------------
#