From c04f6a0b4c067b4098fc841a9dbb8781dcec1c68 Mon Sep 17 00:00:00 2001 From: Jonathan Lee Date: Wed, 7 Dec 2016 22:06:59 -0800 Subject: [PATCH] Specify shell in makefile Summary: The second variable "SHELL" simply tells make explicitly which shell to use, instead of allowing it to default to "/bin/sh", which may or may not be Bash. However, simply defining the second variable by itself causes make to throw an error concerning a circular definition, as it would be attempting to use the "shell" command while simultaneously trying to set which shell to use. Thus, the first variable "BASH_EXISTS" is defined such that make already knows about "/path/to/bash" before trying to use it to set "SHELL". A more technically correct solution would be to edit the makefile itself to make it compatible with non-bash shells (see the original Issue discussion for details). However, as it seems very few of the people working on this project were building with non-bash shells, I figured this solution would be good enough. Closes https://github.com/facebook/rocksdb/pull/1631 Differential Revision: D4295689 Pulled By: yiwu-arbug fbshipit-source-id: e4f9532 --- Makefile | 3 +++ 1 file changed, 3 insertions(+) diff --git a/Makefile b/Makefile index ed0917c37..26b3ddd98 100644 --- a/Makefile +++ b/Makefile @@ -6,6 +6,9 @@ #----------------------------------------------- +BASH_EXISTS := $(shell which bash) +SHELL := $(shell which bash) + CLEAN_FILES = # deliberately empty, so we can append below. CFLAGS += ${EXTRA_CFLAGS} CXXFLAGS += ${EXTRA_CXXFLAGS}