Reconsider Makefile including config from `$HOME`
Closed this issue · 1 comments
WardBrian commented
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
SteveBronder commented
idk anyone that uses this so I'm pretty for removing it