• J
    Specify shell in makefile · c04f6a0b
    Jonathan Lee 提交于
    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
    c04f6a0b
Makefile 49.9 KB