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
This commit is contained in:
parent
45c7ce1377
commit
c04f6a0b4c
Loading…
Reference in New Issue
Block a user