1 files changed, 1 insertions, 1 deletions
diff --git a/Makefile b/Makefile
index aa5bf01c17..6c3a228519 100644
--- a/Makefile
+++ b/Makefile
@@ -9,7 +9,7 @@
 # that you have tools like git, makeinfo and cppi installed.
 
 # Required for the use of <(...) below.
-SHELL=/bin/bash
+SHELL=bash
 
 # Produce some files that are not stored in the repository.
 all: