Reconsider Makefile including config from $HOME #3088
Description
Description
Stan's makefiles include custom configuration from a couple locations.
The first is make/local, and this is what we document and recommend using.
The second is a sub-directory of $HOME:
Line 14 in 4c626fd
This can cause issues when HOME has a space in the path (found by @andrjohns)
I don't think we document this file anywhere, and I also think that allowing a global config like this is probably a bad idea in general.
Current Version:
v4.9.0