From f41557ad13796424692ecca525b58fd03fc9dc7a Mon Sep 17 00:00:00 2001 From: Mohammad Akhlaghi Date: Fri, 27 Jul 2018 12:50:19 +0200 Subject: 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. --- Makefile | 13 +++++++++++++ 1 file changed, 13 insertions(+) (limited to 'Makefile') 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 # -------------------------- # -- cgit v1.2.1